ai.krr.fol
Class QuantifiedSentence

java.lang.Object
  ai.krr.fol.Sentence
      ai.krr.fol.QuantifiedSentence

All Implemented Interfaces:

inf.compilers.SyntaxAdaptable, java.lang.Cloneable, java.lang.Comparable<Sentence>

public class QuantifiedSentence
extends Sentence

Nested Class Summary

static class

QuantifiedSentence.Quantifier This enumeration defines the possible quantifiers that bind variables in the content Sentence.

Nested classes/interfaces inherited from class ai.krr.fol.Sentence

Sentence.SubSentenceIterator

Field Summary

protected Sentence	contained the content Sentence
protected QuantifiedSentence.Quantifier	quantifier the Quantifier for the Variables
protected Variable[]	variables the Variables that are bound

Constructor Summary

QuantifiedSentence(QuantifiedSentence.Quantifier q, Variable[] vars, Sentence content)
This constructor for a QuantifiedSentence takes a Quantifier, a List of Variables, and a Sentence.

QuantifiedSentence(QuantifiedSentence.Quantifier q, Variable var, Sentence content)
This constructor for a QuantifiedSentence takes a Quantifier, a single Variable, and a Sentence.

Method Summary

protected void	addBoundVariables(java.util.Set<Variable> bound) This function adds the bound Variables in this Sentence to the given Set.
protected void	addConstants(java.util.Set<Symbol> sys) This function adds all the constant Symbols used in this Sentence to the given Set.
protected void	addFreeVariables(java.util.Set<Variable> free, java.util.Set<Variable> bound) This function adds the free Variables in this Sentence to the first given Set.
protected void	addFunctions(java.util.Map<Symbol,java.lang.Integer> sys) This function adds all the function Symbols used in this Sentence to the given Set.
protected void	addPredicates(java.util.Map<NamedSymbol,java.lang.Integer> sys) This function adds all the predicate Symbols used in this Sentence to the given Set.
QuantifiedSentence	clone() This function generates a shallow copy of this QuantifiedSentence.
QuantifiedSentence	clone(Substitution s) Returns a copy of this Sentence with Variables replaced according to the given Substitution.
int	compareTo(QuantifiedSentence stmt) This function compares this QuantifiedSentence to the given QuantifiedSentence.
int	compareTo(Sentence stmt) This function compares this Sentence to the given Sentence.
boolean	equals(java.lang.Object obj) This function tests whether this and the given Object are equal.
boolean	equals(QuantifiedSentence other) This function tests whether this and the given Object are equal.
BooleanSymbol	evaluate(Interpretation ipt, Substitution s) This function evaluates this Sentence under the given Interpretation and Substitution for Variables.
boolean	exceedsDepth(int depth) This function tests whether this Sentence exceeds the given depth which should be a non-negative integer.
int	getClassOrderIndex() This function returns the index used for ordering Sentences across different classes.
Sentence	getContent() This function returns the contained Sentence.
int	getDepth() This function returns the nesting depth of this Sentence.
QuantifiedSentence.Quantifier	getQuantifier() This function returns the Quantifier used for the Variables.
Variable[]	getVariables() This function returns the Variables that are bound here.
int	hashCode() This function returns the hash code of this QuantifiedSentence.
protected Sentence	skolemize(boolean isNegated, Term[] uqVars, Substitution s) This function computes a skolemized version of this Sentence.
protected Sentence	toCNF(boolean isNegated) This function returns a new Sentence which is the CNF of this Sentence.
protected Sentence	toDNF(boolean isNegated) This function returns a new Sentence which is the CNF of this Sentence.
java.lang.String	toString() A QuantifiedSentence is printed as:

Methods inherited from class ai.krr.fol.Sentence

allSubSentences, getBoundVariables, getConstants, getFreeVariables, getFunctions, getPredicates, prettyPrint, read, skolemize, toClauseForm, toCNF, toDNF, write

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

quantifier

protected final QuantifiedSentence.Quantifier quantifier

the Quantifier for the Variables

variables

protected final Variable[] variables

the Variables that are bound

contained

protected final Sentence contained

the content Sentence

Constructor Detail

QuantifiedSentence

public QuantifiedSentence(QuantifiedSentence.Quantifier q,
                          Variable var,
                          Sentence content)

This constructor for a QuantifiedSentence takes a Quantifier, a single Variable, and a Sentence.

Parameters:

q - the Quantifier for the Variables

vars - the Variables to which the Quantifier applies

content - the Sentence that should contain the bound Variables

QuantifiedSentence

public QuantifiedSentence(QuantifiedSentence.Quantifier q,
                          Variable[] vars,
                          Sentence content)

This constructor for a QuantifiedSentence takes a Quantifier, a List of Variables, and a Sentence.

Parameters:

q - the Quantifier for the Variables

var - the Variable to which the Quantifier applies

content - the Sentence that should contain the bound Variables

Method Detail

clone

public QuantifiedSentence clone()

This function generates a shallow copy of this QuantifiedSentence. The copy will contain the same Symbols and Variables as the original.

Specified by:

clone in class Sentence

Returns:

an equal copy of this QuantifiedSentence

clone

public QuantifiedSentence clone(Substitution s)

Returns a copy of this Sentence with Variables replaced according to the given Substitution. Symbols in the copy will be the same as the original ones but Variables will be replaced by the respective Terms in the given Substitution. A Variable that is bound here must not occur in the Substitution. It will be replaced by a new (different) Variable with the same name. The given Substitution will be extended to include the mappings of old Variables to new ones.

Specified by:

clone in class Sentence

Parameters:

s - the Substitution that tells us how to replace Variables

Returns:

a new Sentence that is an instance of this Sentence; the Substitution s will be extended with any new Variable replacements introduced

getDepth

public int getDepth()

This function returns the nesting depth of this Sentence. The depth of a quantified Sentence is the depth of the contained Sentences plus the number of quantified variables.

Specified by:

getDepth in class Sentence

Returns:

the depth of this Sentence when seen as a tree

exceedsDepth

public boolean exceedsDepth(int depth)

This function tests whether this Sentence exceeds the given depth which should be a non-negative integer.

Specified by:

exceedsDepth in class Sentence

Parameters:

depth - the depth value that is tested for

Returns:

true iff this.getDepth() > depth

getClassOrderIndex

public final int getClassOrderIndex()

This function returns the index used for ordering Sentences across different classes. This index of this class is defined to be 6.

Specified by:

getClassOrderIndex in class Sentence

Returns:

an integer indicating how this type of Sentence is to be ordered with respect to different types of Sentence

compareTo

public int compareTo(Sentence stmt)

This function compares this Sentence to the given Sentence. The order between different kinds of Sentence is arbitrarily defined as (ascending): TruthValue, Atom, Literal, NegatedSentence, ConnectedSentence, BinaryConnectedSentence, QuantifiedSentence.

Specified by:

compareTo in interface java.lang.Comparable<Sentence>

Specified by:

compareTo in class Sentence

Parameters:

stmt - the Sentence to which this Sentence is to be compared

Returns:

0 if the two Sentences are identical; -1 if the given Sentence should come after this Sentence; and +1 if the given Sentence should come before this Sentence

evaluate

public BooleanSymbol evaluate(Interpretation ipt,
                              Substitution s)

This function evaluates this Sentence under the given Interpretation and Substitution for Variables. Note that the given Substitution must ground all the free Variables occurring in this Sentence. If this Sentence is already ground the given Substitution may be null. If all Atoms and Terms occurring in the Sentence have a value assigned by the Interpretation the result will be a BooleanSymbol. Otherwise it will be null.

Specified by:

evaluate in class Sentence

Parameters:

ipt - the Interpretation giving values for Atoms and Terms

s - the Substitution for Variables occurring in this Term

Returns:

the value of this Term under the given Interpretation

getQuantifier

public final QuantifiedSentence.Quantifier getQuantifier()

This function returns the Quantifier used for the Variables.

Returns:

the Quantifier of this QuantifiedSentence

getVariables

public final Variable[] getVariables()

This function returns the Variables that are bound here.

Returns:

the List of quantified Variables

getContent

public final Sentence getContent()

This function returns the contained Sentence.

Returns:

the Sentence contained in this QuantifiedSentence

compareTo

public int compareTo(QuantifiedSentence stmt)

This function compares this QuantifiedSentence to the given QuantifiedSentence. The order between QuantifiedSentences is primarily defined by the order of the Quantifiers. If they use the same Quantifier the Variables and contained Sentences are compared.

Parameters:

other - the QuantifiedSentence to which this QuantifiedSentence is to be compared

Returns:

0 if the two Sentences are identical; -1 if the given Sentence should come after this Sentence; and +1 if the given Sentence should come before this Sentence

addConstants

protected void addConstants(java.util.Set<Symbol> sys)

This function adds all the constant Symbols used in this Sentence to the given Set.

Specified by:

addConstants in class Sentence

Parameters:

sys - the Set that will contain all the Constants

addFunctions

protected void addFunctions(java.util.Map<Symbol,java.lang.Integer> sys)

This function adds all the function Symbols used in this Sentence to the given Set.

Specified by:

addFunctions in class Sentence

Parameters:

sys - the Set that will contain all the function names

addPredicates

protected void addPredicates(java.util.Map<NamedSymbol,java.lang.Integer> sys)

This function adds all the predicate Symbols used in this Sentence to the given Set.

Specified by:

addPredicates in class Sentence

Parameters:

sys - the Set that will contain all the predicate names

addBoundVariables

protected void addBoundVariables(java.util.Set<Variable> bound)

This function adds the bound Variables in this Sentence to the given Set. These are exactly those Variables that are quantified here.

Specified by:

addBoundVariables in class Sentence

Parameters:

bound - a Set of bound Variables that will be extended

addFreeVariables

protected void addFreeVariables(java.util.Set<Variable> free,
                                java.util.Set<Variable> bound)

This function adds the free Variables in this Sentence to the first given Set. Variables in the second given Set are bound and will not be added.

Specified by:

addFreeVariables in class Sentence

Parameters:

free - a Set of free Variables that will be extended

bound - a Set of bound Variables

skolemize

protected Sentence skolemize(boolean isNegated,
                             Term[] uqVars,
                             Substitution s)

This function computes a skolemized version of this Sentence. It replaces all the existentially quantified variables in this Sentence by appropriate Skolem constants and functions. It all so removes all quantification from this sentence meaning that all remaining Variables are implicitly universally quantified. The given boolean determines whether this sub-Sentence is negated, which is necessary to determine the effective type of quantifier in a QuantifiedSentence. The given Term must all be Variables and represent all the universally quantified Variables at this point. These will be arguments to a potentially introduced Skolem function. Finally, the given Substitution must store mappings from existentially quantified Variables to Skolem Terms.

Specified by:

skolemize in class Sentence

Parameters:

isNegated - whether the Sentence is negated

uqVars - the known universally quantified Variables at this point

s - the Substitution for Variable replacements

Returns:

a new Sentence with no quantification (can be converted to CNF/DNF)

toCNF

protected Sentence toCNF(boolean isNegated)

This function returns a new Sentence which is the CNF of this Sentence. However, quantifiers must not occur in CNF and hence this calling this function will cause an IllegalStateException.

Specified by:

toCNF in class Sentence

Parameters:

isNegated - whether the Sentence is negated

Returns:

a new Sentence which is the CNF of this Sentence, possibly negated

toDNF

protected Sentence toDNF(boolean isNegated)

This function returns a new Sentence which is the CNF of this Sentence. However, quantifiers must not occur in CNF and hence this calling this function will cause an IllegalStateException.

Specified by:

toDNF in class Sentence

Parameters:

isNegated - whether the Sentence is negated

Returns:

a new Sentence which is the CNF of this Sentence, possibly negated

toString

public java.lang.String toString()

A QuantifiedSentence is printed as:

 (( <quantifier> <variable>+ ) <formula> )
 

Overrides:

toString in class java.lang.Object

Returns:

the String that represents this QuantifiedSentence

equals

public boolean equals(java.lang.Object obj)

This function tests whether this and the given Object are equal. In general, two QuantifiedSentences are equal if they have the same quantifier, all the variables in the same order and equal, and the contained Sentences are equal.

Overrides:

equals in class java.lang.Object

Parameters:

other - the Sentence this one is to be compared to

Returns:

whether the given Object is equal to this one

equals

public boolean equals(QuantifiedSentence other)

This function tests whether this and the given Object are equal. In general, two QuantifiedSentences are equal if they have the same quantifier, all the variables in the same order and equal, and the contained Sentences are equal.

Parameters:

other - the Sentence this one is to be compared to

Returns:

whether the given Object is equal to this one

hashCode

public int hashCode()

This function returns the hash code of this QuantifiedSentence.

Overrides:

hashCode in class java.lang.Object

Returns:

a positive integer that may be used for hashing