ai.krr.propositions
Class Sentence

java.lang.Object
  ai.krr.propositions.Sentence

All Implemented Interfaces:

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

Direct Known Subclasses:

Atom, ConnectedSentence, Literal, NegatedSentence, 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 propositional 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

Constructor Summary

Sentence()

Method Summary

abstract void	addPropositions(java.util.Set<NamedSymbol> props) This function adds the propositions contained in this Sentence to the given Set.
protected void	addSubSentences(java.util.List<Sentence> sents, boolean rootFirst) This function can be used to fill the given List of with all the sub-Sentences of this Sentence, including the Sentence itself.
java.util.List<Sentence>	allSubSentences(boolean rootFirst) This function can be used to create a List of all the sub-Sentences of this Sentence, including the Sentence itself.
abstract Sentence	clone() This function generates a deep copy of this Sentence.
abstract int	compareTo(Sentence stmt) This function compares this Sentence to the given Sentence.
abstract BooleanSymbol	evaluate(Interpretation i) This function evaluates this Sentence under the given Interpretation.
boolean	exceedsDepth(int depth) This function tests whether this Sentence exceeds the given depth which should be a non-negative integer.
abstract int	getClassOrderIndex() This function returns the index used for ordering Sentences across different classes.
int	getDepth() This function returns the nesting depth of this Sentence.
java.util.Set<NamedSymbol>	getPropositions() This function returns the set of propositional symbols that occur in this Sentence.
boolean	isAtom() This function tests whether this Sentence is an Atom.
boolean	isLiteral() This function tests whether this Sentence is a Literal.
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)
java.util.List<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()

This function generates a deep copy of this Sentence. The copy will contain the same Symbols as the original.

Overrides:

clone in class java.lang.Object

Returns:

an equal copy of this 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.

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

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

addPropositions

public abstract void addPropositions(java.util.Set<NamedSymbol> props)

This function adds the propositions contained in this Sentence to the given Set. The boolean propositions TRUE and FALSE will not be added to the set.

Parameters:

props - the Set to which the propositional symbols are added

evaluate

public abstract BooleanSymbol evaluate(Interpretation i)

This function evaluates this Sentence under the given Interpretation. If all propositions occurring in the Sentence have a truth value assigned by the Interpretation the result will be either BooleanSymbol.TRUE or BooleanSymbol.FALSE.

Parameters:

i - the Interpretation giving truth values for propositions

Returns:

the truth value of this Sentence under the given Interpretation

isAtom

public boolean isAtom()

This function tests whether this Sentence is an Atom. This default implementation always returns false. /p>

Returns:

true if and only if this is an Atom

isLiteral

public boolean isLiteral()

This function tests whether this Sentence is a Literal. This default implementation always returns false.

Returns:

true if and only if this is a Literal

getDepth

public int getDepth()

This function returns the nesting depth of this Sentence. The depth of a TruthValue, an Atom or a Literal is defined to be 0. 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. This default implementation returns 0.

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. The default implementation provided here returns whether the given integer is negative.

Parameters:

depth - the depth value that is tested for

Returns:

true iff this.getDepth() > depth

getPropositions

public java.util.Set<NamedSymbol> getPropositions()

This function returns the set of propositional symbols that occur in this Sentence. The boolean propositions TRUE and FALSE will not be contained in the result.

Returns:

the Set of all the propositional symbols contained in this Sentence

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

Returns:

a List 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.List<Sentence> allSubSentences(boolean rootFirst)

This function can be used to create a List of all the sub-Sentences of this Sentence, including the Sentence itself. If the given boolean is true, a Sentence will preceed its sub-Sentences, otherwise it will succeed them. For a shallow Iterator over a ConnectedSentence see ConnectedSentence.sentences.

Parameters:

rootFirst - true means Sentence before its sub-Sentences

Returns:

an Iterator over all the sub-Sentences of this Sentence

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

addSubSentences

protected void addSubSentences(java.util.List<Sentence> sents,
                               boolean rootFirst)

This function can be used to fill the given List of with all the sub-Sentences of this Sentence, including the Sentence itself. If the given boolean is true, a Sentence will preceed its sub-Sentences, otherwise it will succeed them. This function performs a complete traversal of this Sentence as a tree, down to the level of Literals, Atoms and TruthValues.

Parameters:

sents - the List to add the sub-Sentences to

rootFirst - true means Sentence before its sub-Sentences

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