ai.krr.fol
Class Literal

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

All Implemented Interfaces:

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

public class Literal
extends Sentence

A Literal is one of the most basic building blocks for a Sentence. It simply consists of a predicate over some arguments that may be negated.

Author:

Gerhard Wickler

Nested Class Summary

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

Sentence.SubSentenceIterator

Constructor Summary

Literal(boolean sign, NamedSymbol pSymbol, java.util.List<Term> someTerms)
This constructor for a Literal takes a boolean sign, a predicate Symbol and a List of argument Terms.

Literal(boolean sign, NamedSymbol pSymbol, Term... someTerms)
This constructor for a Literal takes a boolean sign, a predicate Symbol and a number of argument Terms.

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 Term 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 Term 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 Term to the given Set.
Literal	clone() Returns a shallow copy of this Literal.
Literal	clone(Substitution s)
int	compareTo(Literal other) This function compares this Literal to the given Literal.
int	compareTo(Sentence other) This function compares this Literal to the given Sentence.
boolean	complements(Literal other) A Literal is equal to another Literal that consists of a different sign and equal predicate symbol followed by an equal number of equal Terms.
boolean	complements(Literal other, Substitution s) This function attempts to extend the given Substitution so that this Literal and the given Literal are complementary.
boolean	equals(Literal other) A Literal is equal to any other Literal that consists of an equal sign and predicate symbol followed by an equal number of equal Terms.
boolean	equals(java.lang.Object obj) A Literal is only equal to another Literal.
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.
Term[]	getArguments() This function returns the argument Terms of this Atom.
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.
NamedSymbol	getPredicate() This function returns the predicate symbol used in this Atom which is a NamedSymbol.
int	hashCode() This function returns the cashed hash code of this Literal.
boolean	isFunctionFree() This function tests whether this Atom contains any FunctionTerms.
boolean	isGround() This function tests whether this Atom contains any Variables.
boolean	isPositive() This function tests whether this is a positive Literal.
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 Literal which contains the proposition contained in this Atom.
protected Sentence	toDNF(boolean isNegated) This function returns a new Literal which contains the proposition contained in this Atom.
java.lang.String	toString() A Literal is printed as {+|-} <predicate> ( <Term>+ ).
boolean	unify(Literal other, Substitution s) This function attempts to extend the given Substitution so that this Literal and the given Literal are unified.

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

Literal

public Literal(boolean sign,
               NamedSymbol pSymbol,
               java.util.List<Term> someTerms)

This constructor for a Literal takes a boolean sign, a predicate Symbol and a List of argument Terms.

Parameters:

sign - true if and only if this is a positive Literal

pSymbol - the predicate symbol

someTerms - the List of argument Terms

Literal

public Literal(boolean sign,
               NamedSymbol pSymbol,
               Term... someTerms)

This constructor for a Literal takes a boolean sign, a predicate Symbol and a number of argument Terms.

Parameters:

sign - true if and only if this is a positive Literal

pSymbol - the function symbol

someTerms - the argument Terms

Method Detail

clone

public Literal clone()

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

Specified by:

clone in class Sentence

Returns:

an equal copy of this Literal

clone

public Literal clone(Substitution s)

Returns a deep copy of this Literal 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. The function uses Term.clone(Substitution) to generate the copies of all the argument Terms in this Atom.

Specified by:

clone in class Sentence

Parameters:

s - the Substitution that tells us how to replace Variables

Returns:

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

getDepth

public int getDepth()

This function returns the nesting depth of this Sentence. The depth of a Literal is the depth of the deepest Term it contains plus one if it is positive, otherwise plus two.

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

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 other)

This function compares this Literal 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:

other - the Sentence to which this Literal is to be compared

Returns:

0 if the two Literals are equal; -1 if the given Sentence should come after this Literal; and +1 if the given Sentence should come before this Literal

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

isPositive

public final boolean isPositive()

This function tests whether this is a positive Literal.

Returns:

whether this Literal is positive, i.e. not negated

getPredicate

public final NamedSymbol getPredicate()

This function returns the predicate symbol used in this Atom which is a NamedSymbol.

Returns:

the predicate used in this Atom

getArguments

public final Term[] getArguments()

This function returns the argument Terms of this Atom.

Returns:

the arguments of this Atom

isFunctionFree

public boolean isFunctionFree()

This function tests whether this Atom contains any FunctionTerms. This is true only if none of the arguments is a FunctionTerm.

Returns:

true iff this Atom contains no FunctionTerms

isGround

public boolean isGround()

This function tests whether this Atom contains any Variables. This is true only if one of the arguments contains a Variable.

Returns:

true iff this Atom contains no VariableTerms

unify

public boolean unify(Literal other,
                     Substitution s)

This function attempts to extend the given Substitution so that this Literal and the given Literal are unified. It returns true if and only if this is possible. Unification succeeds only if the two signs and predicate symbols are equal and the Substitution can be extended to unify all arguments.

Parameters:

other - the other Literal this Literal is to be unified with

s - the Substitution to be extended for the unification

Returns:

whether a unifying extension of the given Substitution was possible

complements

public boolean complements(Literal other)

A Literal is equal to another Literal that consists of a different sign and equal predicate symbol followed by an equal number of equal Terms.

Parameters:

other - the Literal this Literal is compared to

Returns:

whether the given Literal is complementary to this one

complements

public boolean complements(Literal other,
                           Substitution s)

This function attempts to extend the given Substitution so that this Literal and the given Literal are complementary. It returns true if and only if this is possible. It succeeds only if the two signs are different, the predicate symbols are equal and the Substitution can be extended to unify all arguments.

Parameters:

other - the other Literal this Literal is to be unified with

s - the Substitution to be extended for the unification

Returns:

whether a unifying extension of the given Substitution was possible

compareTo

public int compareTo(Literal other)

This function compares this Literal to the given Literal. The order between Literals is primarily defined by the order of the predicate symbols and the argument Terms they contain. First the predicate symbols are compared. Next, the signs are compared. Then the first argument Terms are compared and if they are equal the second argument Terms are compared etc. It is like an alphabetical sorting.

Parameters:

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

Returns:

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

addConstants

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

This function adds all the constant Symbols used in this Term 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 Term 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 Term 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.

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 final void addBoundVariables(java.util.Set<Variable> bound)

This function adds the bound Variables in this Sentence to the given Set. This implementation does not modify 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 returns a Literal that has a sign according to the given boolean, the predicate from this Atom, and clones of the arguments under the given Substitution.

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 Literal which contains the proposition contained in this Atom. The given boolean indicates whether the new Literal is to be negated.

Specified by:

toCNF in class Sentence

Parameters:

isNegated - whether the Literal has to be negated

Returns:

a new Literal, possibly negative

toDNF

protected Sentence toDNF(boolean isNegated)

This function returns a new Literal which contains the proposition contained in this Atom. The given boolean indicates whether the new Literal is to be negated.

Specified by:

toDNF in class Sentence

Parameters:

isNegated - whether the Literal has to be negated

Returns:

a new Literal, possibly negative

toString

public java.lang.String toString()

A Literal is printed as {+|-} <predicate> ( <Term>+ ).

Overrides:

toString in class java.lang.Object

Returns:

the String that represents this Atom

equals

public boolean equals(java.lang.Object obj)

A Literal is only equal to another Literal.

Overrides:

equals in class java.lang.Object

Parameters:

obj - the Object this Literal is compared to

Returns:

whether the given Object equals this Literal

equals

public boolean equals(Literal other)

A Literal is equal to any other Literal that consists of an equal sign and predicate symbol followed by an equal number of equal Terms.

Parameters:

other - the Object this Literal is compared to

Returns:

whether the given Object equals this Atom

hashCode

public final int hashCode()

This function returns the cashed hash code of this Literal.

Overrides:

hashCode in class java.lang.Object

Returns:

a positive integer that may be used for hashing