ai.krr.fol
Class Sentence

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

All Implemented Interfaces:

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

Direct Known Subclasses:

Atom, ConnectedSentence, Literal, NegatedSentence, QuantifiedSentence, TruthValue

public abstract class Sentence
extends java.lang.Object
implements java.lang.Cloneable, java.lang.Comparable<Sentence>, inf.compilers.SyntaxAdaptable

A Sentence is usually used in logic to represent a proposition that is either true or false. More formally, a Sentence in first-order logic is a syntactic expression that has a truth value under a given interpretation. Currently, there are several kinds of Sentence implemented.

Author:

Gerhard Wickler

Nested Class Summary

(package private) class

Sentence.SubSentenceIterator

Constructor Summary

Sentence()

Method Summary

protected abstract void	addBoundVariables(java.util.Set<Variable> bound) This function adds the bound Variables in this Sentence to the given Set.
protected abstract void	addConstants(java.util.Set<Symbol> sys) This function adds all the constant Symbols used in this Sentence to the given Set.
protected abstract 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 abstract 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 abstract 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.
java.util.Iterator<Sentence>	allSubSentences() This function can be used to iterate through all the sub-Sentences of this Sentence, including the Sentence itself.
abstract Sentence	clone() Returns a copy of this Sentence.
abstract Sentence	clone(Substitution s) Returns a copy of this Sentence with free Variables replaced according to the given Substitution.
abstract int	compareTo(Sentence stmt) This function compares this Sentence to the given Sentence.
abstract BooleanSymbol	evaluate(Interpretation ipt, Substitution s) This function evaluates this Sentence under the given Interpretation and Substitution for Variables.
abstract boolean	exceedsDepth(int depth) This function tests whether this Sentence exceeds the given depth which should be a non-negative integer.
java.util.Set<Variable>	getBoundVariables() This function adds all the bound Variables in this Sentence to the returned Set.
abstract int	getClassOrderIndex() This function returns the index used for ordering Sentences across different classes.
protected java.util.Set<Symbol>	getConstants() This function returns a set of all the constant Symbols occurring in this Sentence.
abstract int	getDepth() This function returns the nesting depth of this Sentence.
java.util.Set<Variable>	getFreeVariables() This function adds all the free Variables in this Sentence to the returned Set.
protected java.util.Map<Symbol,java.lang.Integer>	getFunctions() This function returns a set of all the function Symbols occurring in this Sentence.
protected java.util.Map<NamedSymbol,java.lang.Integer>	getPredicates() This function returns a set of all the predicate Symbols occurring in this Sentence.
void	prettyPrint(int indent, java.io.Writer w, inf.compilers.SyntaxAdaptor sa) This function can be used write this SyntaxAdaptable object to the given Writer.
static Sentence	read(java.io.Reader r, inf.compilers.SyntaxAdaptor<Sentence> sa)
Sentence	skolemize() This function computes a skolemized version of this Sentence.
protected abstract Sentence	skolemize(boolean isNegated, Term[] uqVars, Substitution s) This function computes a skolemized version of this Sentence.
java.util.Set<Clause>	toClauseForm() This function converts this Sentence into an equivalent Set of Clauses.
Sentence	toCNF() This function returns a new Sentence which is the CNF of this Sentence.
protected abstract Sentence	toCNF(boolean isNegated) This function returns a new Sentence which is the CNF of this Sentence.
Sentence	toDNF() This function returns a new Sentence which is the DNF of this Sentence.
protected abstract Sentence	toDNF(boolean isNegated) This function returns a new Sentence which is the DNF of this Sentence.
void	write(java.io.Writer w, inf.compilers.SyntaxAdaptor sa) This function can be used write this logical Sentence to the given Writer.

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Sentence

public Sentence()

Method Detail

clone

public abstract Sentence clone()

Returns a copy of this Sentence. Variables and Symbols in the copy will be the same as the original ones.

Overrides:

clone in class java.lang.Object

Returns:

an equal copy of this Sentence

clone

public abstract Sentence clone(Substitution s)

Returns a copy of this Sentence with free 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 not occurring in the Substitution 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.

This function can also be used to generate a copy of this Sentence that contains a new set of Variables. The given Substitution should be a new, empty Substitution in this case. Otherwise cloning can be seen as instantiating the 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 abstract int getDepth()

This function returns the nesting depth of this Sentence. The depth of a TruthValue is defined to be 0. The depth of an Atom or a Literal is the depth of the deepest Term it contains. The depth of a negated sentence is the depth of the contained Sentence. The depth of a conjunction, disjunction, or implication is the maximum depth of the sub-Sentences plus 1. The depth of a co-implication or exclusive disjunction is the maximum depth of the sub-Sentences plus 2. Finally, the depth of a quantified Sentence is the depth of the contained Sentence plus 1.

Returns:

the depth of this Sentence when seen as a tree

exceedsDepth

public abstract boolean exceedsDepth(int depth)

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

Parameters:

depth - the depth value that is tested for

Returns:

true iff this.getDepth() > depth

getClassOrderIndex

public abstract int getClassOrderIndex()

This function returns the index used for ordering Sentences across different classes.

Returns:

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

compareTo

public abstract 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>

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 abstract 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.

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

getFreeVariables

public java.util.Set<Variable> getFreeVariables()

This function adds all the free Variables in this Sentence to the returned Set. Note: A Variable may be both, free and bound, in a Sentence.

Returns:

a Set containing all free Variables occurring in this Sentence

getBoundVariables

public java.util.Set<Variable> getBoundVariables()

This function adds all the bound Variables in this Sentence to the returned Set. Note: A Variable may be both, free and bound, in a Sentence.

Returns:

a Set containing all Variables bound in this Sentence

skolemize

public Sentence skolemize()

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 also removes all quantification from this sentence meaning that all remaining Variables are implicitly universally quantified. If this Sentence contains free Variables they are treated as implicitly universally quantified at top level (meaning they will end up in every Skolem function).

Returns:

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

toCNF

public Sentence toCNF()

This function returns a new Sentence which is the CNF of this Sentence. This is done by:

1. replacing the connectives IMPLIES, IFF, and XOR by their equivalent combinations of AND and OR; this may lead to a multiplication of sub-sentences;
2. pulling the negations into the Sentence using mainly de Morgan's law;

Returns:

a new Sentence which is the CNF of this Sentence

toDNF

public Sentence toDNF()

This function returns a new Sentence which is the DNF of this Sentence. This is done by:

1. replacing the connectives IMPLIES, IFF, and XOR by their equivalent combinations of AND and OR; this may lead to a multiplication of sub-sentences;
2. pulling the negations into the Sentence using mainly de Morgan's law;

Returns:

a new Sentence which is the DNF of this Sentence

toClauseForm

public java.util.Set<Clause> toClauseForm()

This function converts this Sentence into an equivalent Set of Clauses. To achieve this, this Sentence is first converted to CNF. If this results in TruthValue.TRUE, an empty Set will be returned. If this results in TruthValue.FALSE, the returned Set will contain exactly one Clause which will be the empty Clause. Otherwise the returned Set will contain at least one Clause and none of the returned Clauses will be empty.

Note: This Sentence must not contain any quantification. No skolemization is performed here!

Returns:

a Set of Clauses that is equivalent to this Sentence

write

public void write(java.io.Writer w,
                  inf.compilers.SyntaxAdaptor sa)
           throws inf.compilers.ExpressivenessException,
                  java.io.IOException

This function can be used write this logical Sentence to the given Writer. The syntax in which it is written is defined by the SyntaxAdaptor that is also given to this function.

Specified by:

write in interface inf.compilers.SyntaxAdaptable

Parameters:

w - the Writer to which this Sentence is written

sa - the SyntaxAdaptor that determines the syntax

Throws:

inf.compilers.ExpressivenessException - if the syntax does not support every construct occurring in this Sentence

java.io.IOException - if writing to the Writer fails

prettyPrint

public void prettyPrint(int indent,
                        java.io.Writer w,
                        inf.compilers.SyntaxAdaptor sa)
                 throws inf.compilers.ExpressivenessException,
                        java.io.IOException

This function can be used write this SyntaxAdaptable object to the given Writer. The syntax is the same as for normal writing. The only difference is the inclusion of extra space and newlines for better readability.

Specified by:

prettyPrint in interface inf.compilers.SyntaxAdaptable

Parameters:

indent - the amount of indentation for the first line

w - the Writer to which this Sentence is written

sa - the SyntaxAdaptor that determines the syntax

Throws:

inf.compilers.ExpressivenessException - if the syntax does not support every construct occurring in this Sentence

java.io.IOException - if writing to the Writer fails

allSubSentences

public java.util.Iterator<Sentence> allSubSentences()

This function can be used to iterate through all the sub-Sentences of this Sentence, including the Sentence itself. The returned Iterator first enumerates all the children of a Sentence before the sentence itself. It performs a complete traversal of this Sentence as a tree, down to the level of Literals, Atoms and TruthValues. For a shallow Iterator over a ConnectedSentence see ConnectedSentence#subSentences.

Returns:

an Iterator over all the sub-Sentences of this Sentence

addConstants

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

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

Parameters:

sys - the Set that will contain all the Constants

addFunctions

protected abstract 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.

Parameters:

sys - the Set that will contain all the function names

addPredicates

protected abstract 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.

Parameters:

sys - the Set that will contain all the predicate names

addFreeVariables

protected abstract 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.

Parameters:

free - a Set of free Variables that will be extended

bound - a Set of bound Variables

addBoundVariables

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

This function adds the bound Variables in this Sentence to the given Set.

Parameters:

bound - a Set of bound Variables that will be extended

skolemize

protected abstract 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 also 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.

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 abstract Sentence toCNF(boolean isNegated)

This function returns a new Sentence which is the CNF of this Sentence. The given boolean indicates whether the Sentence is to be treated as negated at this point.

Parameters:

isNegated - whether the Sentence is negated

Returns:

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

toDNF

protected abstract Sentence toDNF(boolean isNegated)

This function returns a new Sentence which is the DNF of this Sentence. The given boolean indicates whether the Sentence is to be treated as negated at this point.

Parameters:

isNegated - whether the Sentence is negated

Returns:

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

getConstants

protected java.util.Set<Symbol> getConstants()

This function returns a set of all the constant Symbols occurring in this Sentence.

Returns:

a Set of all the constant Symbols in this Sentence

getFunctions

protected java.util.Map<Symbol,java.lang.Integer> getFunctions()

This function returns a set of all the function Symbols occurring in this Sentence. Each function is mapped to its arity.

Returns:

a Set of all the function Symbols in this Sentence

getPredicates

protected java.util.Map<NamedSymbol,java.lang.Integer> getPredicates()

This function returns a set of all the predicate Symbols occurring in this Sentence.

Returns:

a Set of all the predicate Symbols in this Sentence

read

public static Sentence read(java.io.Reader r,
                            inf.compilers.SyntaxAdaptor<Sentence> sa)
                     throws inf.compilers.ExpressivenessException,
                            java.text.ParseException,
                            java.io.IOException

Throws:

inf.compilers.ExpressivenessException

java.text.ParseException

java.io.IOException