ai.krr.fol
Class ConnectedSentence

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

All Implemented Interfaces:

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

Direct Known Subclasses:

BinaryConnectedSentence

public class ConnectedSentence
extends Sentence

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

Author:

Gerhard Wickler

Nested Class Summary

static class

ConnectedSentence.Connective This enumeration defines the possible connectives that can connect the sub-Sentences.

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

Sentence.SubSentenceIterator

Field Summary

protected ConnectedSentence.Connective	connective the connective for this Sentence
protected Sentence[]	sentences the sub-Sentences connected here

Constructor Summary

	ConnectedSentence(ConnectedSentence.Connective connective, java.util.List<Sentence> sents) This constructor for a ConnectedSentence takes a Connective and a List of Sentences which are the Sentences that are connected by the given connective.
	ConnectedSentence(ConnectedSentence.Connective connective, Sentence... sentences) This constructor for a ConnectedSentence takes a Connective and a number of Sentences which are the Sentences that are connected by the given connective.
protected	ConnectedSentence(Sentence s1, ConnectedSentence.Connective connective, Sentence s2) This constructor for a ConnectedSentence takes a Connective and two Sentences which are the Sentences that are connected by the given connective.

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.
ConnectedSentence	clone() This function generates a shallow copy of this ConnectedSentence.
ConnectedSentence	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 ConnectedSentence to the given ConnectedSentence.
int	compareTo(Sentence stmt) This function compares this Sentence to the given Sentence.
boolean	equals(ConnectedSentence other) This function tests whether this and the given Object are equal.
boolean	equals(java.lang.Object obj) 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.
ConnectedSentence.Connective	getConnective() This function returns the Connective that connects the sub-Sentences in this ConnectedSentence.
int	getDepth() This function returns the nesting depth of this Sentence.
Sentence[]	getSubSentences() This function returns the the sub-Sentences that are joined in this ConnectedSentence.
int	hashCode() This function returns the hash code of this ConnectedSentence.
boolean	isConjunction() This function tests whether this Sentence is a conjunction.
boolean	isDisjunction() This function tests whether this Sentence is a disjunction.
(package private) static java.util.List<java.util.List<Literal>>	multiplyS(java.util.List<java.util.List<Literal>> nf, ConnectedSentence lits) This function multiplies the given List of List of Literals with the given 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 form of this ConnectedSentence.
protected Sentence	toDNF(boolean isNegated) This function returns a new Sentence which is the CNF form of this AndOrSentence.
java.lang.String	toString() A ConnectedSentence 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

connective

protected final ConnectedSentence.Connective connective

the connective for this Sentence

sentences

protected final Sentence[] sentences

the sub-Sentences connected here

Constructor Detail

ConnectedSentence

public ConnectedSentence(ConnectedSentence.Connective connective,
                         java.util.List<Sentence> sents)

This constructor for a ConnectedSentence takes a Connective and a List of Sentences which are the Sentences that are connected by the given connective. The connective should be AND or OR.

Parameters:

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

sents - the Sentences to be connected here

ConnectedSentence

public ConnectedSentence(ConnectedSentence.Connective connective,
                         Sentence... sentences)

This constructor for a ConnectedSentence takes a Connective and a number of Sentences which are the Sentences that are connected by the given connective. The connective should be AND or OR.

Parameters:

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

sentences - the Sentences to be connected here

ConnectedSentence

protected ConnectedSentence(Sentence s1,
                            ConnectedSentence.Connective connective,
                            Sentence s2)

This constructor for a ConnectedSentence takes a Connective and two Sentences which are the Sentences that are connected by the given connective.

Parameters:

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

s1 - the first Sentence to be connected here

s2 - the second Sentence to be connected here

Method Detail

clone

public ConnectedSentence clone()

This function generates a shallow copy of this ConnectedSentence. The copy will contain the same sub-Sentences as the original.

Specified by:

clone in class Sentence

Returns:

an equal copy of this ConnectedSentence

clone

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

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 conjunction or disjunction is the maximum depth of the sub-Sentences plus 1.

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

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.

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

getConnective

public final ConnectedSentence.Connective getConnective()

This function returns the Connective that connects the sub-Sentences in this ConnectedSentence.

Returns:

the Connective of this ConnectedSentence

getSubSentences

public final Sentence[] getSubSentences()

This function returns the the sub-Sentences that are joined in this ConnectedSentence.

Returns:

the sub-Sentences of this ConnectedSentence

isConjunction

public boolean isConjunction()

This function tests whether this Sentence is a conjunction.

Returns:

whether this Sentence is a conjunction

isDisjunction

public boolean isDisjunction()

This function tests whether this Sentence is a disjunction.

Returns:

whether this Sentence is a disjunction

compareTo

public int compareTo(ConnectedSentence other)

This function compares this ConnectedSentence to the given ConnectedSentence. The order between ConnectedSentence 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.

Parameters:

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

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. Newly bound Variables will also be added to the second Set.

Specified by:

addFreeVariables in class Sentence

Parameters:

free - a Set of free Variables that will be extended

bound - a Set of bound Variables

addBoundVariables

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

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

Specified by:

addBoundVariables in class Sentence

Parameters:

bound - a Set of bound Variables that will be extended

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

Specified by:

toCNF in class Sentence

Parameters:

isNegated - whether the Sentence is negated

Returns:

a new ConnectedSentence which is the CNF of this Sentence

toDNF

protected Sentence toDNF(boolean isNegated)

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

Specified by:

toDNF in class Sentence

Parameters:

isNegated - whether the Sentence is negated

Returns:

a new AndOrSentence which is the DNF of this Sentence

toString

public java.lang.String toString()

A ConnectedSentence is printed as:

 ( <connective> <formula>+ )
 

Overrides:

toString in class java.lang.Object

Returns:

the String that represents this ConnectedSentence

equals

public boolean equals(java.lang.Object obj)

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 java.lang.Object

Parameters:

obj - the Object this one is to be compared to

Returns:

whether the given Object is equal to this one

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.

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 java.lang.Object

Returns:

a positive integer that may be used for hashing

multiplyS

static java.util.List<java.util.List<Literal>> multiplyS(java.util.List<java.util.List<Literal>> nf,
                                                         ConnectedSentence lits)

This function multiplies the given List of List of Literals with the given ConnectedSentence.

Multiplication here is defined as follows: Given a ConnectedSentence of n Literals, the result will contain n times the number of sub-Lists it contained previously, and each copy will be extended with a different Literal from the given ConnectedSentence. For example, multiplying

 ((+A1 +A2) (+B1 +B2))
 

with (AND +C, +D) will result in:

 ((+A1 +A2 +C) (+A1 +A2 +D) (+B1 +B2 +C) (+B1 +B2 +D))
 

Parameters:

lits - a Collection of Literals to multiply this AndOrSentence with