ai.krr.fol
Class BinaryConnectedSentence

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

All Implemented Interfaces:

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

public class BinaryConnectedSentence
extends ConnectedSentence

This class represents a Sentence that consists of a Connective that connects two sub-Sentences. The Connective that may be given to the public constructor must be IMPLIES, IFF or XOR. ConnectedSentences based on AND or OR must be constructed as ConnectedSentences.

Author:

Gerhard Wickler

Nested Class Summary

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

ConnectedSentence.Connective

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

Sentence.SubSentenceIterator

Field Summary

Fields inherited from class ai.krr.fol.ConnectedSentence

connective, sentences

Constructor Summary

BinaryConnectedSentence(Sentence lhs, ConnectedSentence.Connective connective, Sentence rhs)
This constructor for a BinaryConnectedSentence takes a Connective and two Sentences which are the Sentences that are connected by the given connective.

Method Summary

BinaryConnectedSentence	clone() This function generates a deep copy of this BinaryConnectedSentence.
BinaryConnectedSentence	clone(Substitution s) Returns a copy of this Sentence with Variables replaced according to the given Substitution.
int	compareTo(ConnectedSentence other) This function compares this BinaryConnectedSentence to the given ConnectedSentence.
boolean	equals(ConnectedSentence 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.
boolean	exceedsDepth(int depth) This function tests whether this Sentence exceeds the given depth which should be a non-negative integer.
int	getDepth() This function returns the nesting depth of this Sentence.
Sentence	getLeftHandSide() This function returns the left-hand side sub-Sentence of this BinaryConnectedSentence.
Sentence	getRightHandSide() This function returns the right-hand side sub-Sentence of this BinaryConnectedSentence.
int	hashCode() This function returns the hash code of this ConnectedSentence.
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 DNF of this Sentence.

Methods inherited from class ai.krr.fol.ConnectedSentence

addBoundVariables, addConstants, addFreeVariables, addFunctions, addPredicates, compareTo, equals, getClassOrderIndex, getConnective, getSubSentences, isConjunction, isDisjunction, multiplyS, toString

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

Constructor Detail

BinaryConnectedSentence

public BinaryConnectedSentence(Sentence lhs,
                               ConnectedSentence.Connective connective,
                               Sentence rhs)

This constructor for a BinaryConnectedSentence takes a Connective and two Sentences which are the Sentences that are connected by the given connective. The first Sentence is taken to be the left hand side where that matters. The connective should be IMPLIES, IFF or XOR.

Parameters:

lhs - the left hand side sub-Sentence

connective - the connective (e.g. Connective.AND)

rhs - the right hand side sub-Sentence

Method Detail

clone

public BinaryConnectedSentence clone()

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

Overrides:

clone in class ConnectedSentence

Returns:

an equal copy of this BinaryConnectedSentence

clone

public BinaryConnectedSentence 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 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.

Overrides:

clone in class ConnectedSentence

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

Overrides:

getDepth in class ConnectedSentence

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.

Overrides:

exceedsDepth in class ConnectedSentence

Parameters:

depth - the depth value that is tested for

Returns:

true iff this.getDepth() > depth

evaluate

public BooleanSymbol evaluate(Interpretation ipt,
                              Substitution s)

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. Otherwise the result may be null, indicating the truth value of this Sentence is undefined under the given Interpretation. For a BinaryConnectedSentence the returned truth value depends on the connective. It will be BooleanSymbol.TRUE iff:

• the connective is IMPLIES and: the left sub-sentence is false or the right sub-sentence is true; or
• the connective is IFF and the left and right sub-sentences have the same truth value; or
• the connective is XOR and the left and right sub-sentences have different truth value.

Overrides:

evaluate in class ConnectedSentence

Parameters:

ipt - the Interpretation giving truth values for propositions

s - the Substitution for Variables occurring in this Term

Returns:

the truth value of this Sentence under the given Interpretation

getLeftHandSide

public Sentence getLeftHandSide()

This function returns the left-hand side sub-Sentence of this BinaryConnectedSentence. This could be for example, the premise of an implication.

Returns:

the first sub-Sentence connected here

getRightHandSide

public Sentence getRightHandSide()

This function returns the right-hand side sub-Sentence of this BinaryConnectedSentence. This could be for example, the conclusion of an implication.

Returns:

the second sub-Sentence connected here

compareTo

public int compareTo(ConnectedSentence other)

This function compares this BinaryConnectedSentence to the given ConnectedSentence. The order between ConnectedSentences is primarily defined by the order of the Connectives they contain. If they use the same connective a lexical ordering is used, i.e. first the first sub-Sentences are compared. If they are different this determines the overall result, otherwise the second sub-Sentences are compared, etc.

Overrides:

compareTo in class ConnectedSentence

Parameters:

other - the ConnectedSentence to which this BinaryConnectedSentence 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

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.

Overrides:

skolemize in class ConnectedSentence

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. The given boolean indicates whether the Sentence is to be treated as negated at this point.

Overrides:

toCNF in class ConnectedSentence

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 DNF of this Sentence. The given boolean indicates whether the Sentence is to be treated as negated at this point.

Overrides:

toDNF in class ConnectedSentence

Parameters:

isNegated - whether the Sentence is negated

Returns:

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

equals

public boolean equals(ConnectedSentence other)

This function tests whether this and the given Object are equal. In general, two ConnectedSentences are equal if they have the same connective and all the sub-Sentences are in the same order and equal.

Overrides:

equals in class ConnectedSentence

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

Overrides:

hashCode in class ConnectedSentence

Returns:

a positive integer that may be used for hashing