ai.krr.propositions
Class InterpretationEnumerator

java.lang.Object
  ai.krr.propositions.InterpretationEnumerator

All Implemented Interfaces:

TheoremProver

public class InterpretationEnumerator
extends java.lang.Object
implements TheoremProver

This class is a very simple and inefficient TheoremProver that enumerates all possible Interpretation to find models that satisfy or falsify a given Sentence.

Author:

Gerhard Wickler

Constructor Summary

InterpretationEnumerator()

Method Summary

boolean	equivalent(Sentence stmt1, Sentence stmt2) This function tests whether the two given Sentences are equivalent.
boolean	follows(Sentence stmt, java.util.Collection<Sentence> axioms) This function tests whether the given Sentence logically follows from the given Collection of Sentences.
Interpretation	getModel(Sentence stmt) This function attempts to find a model for the given Sentence.
boolean	isInconsistent(Sentence stmt) This function tests whether the given Sentence in propositional logic is inconsistent.
boolean	isValid(Sentence stmt) This function tests whether the given Sentence in propositional logic is valid.

Methods inherited from class java.lang.Object

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

Constructor Detail

InterpretationEnumerator

public InterpretationEnumerator()

Method Detail

isValid

public boolean isValid(Sentence stmt)

This function tests whether the given Sentence in propositional logic is valid. A Sentence is valid if and only if it is true under all possible Interpretations. This method loops over all possible Interpretations until it finds one that falsifies the given Sentence, in which case it returns false. Only if no such Interpretation can be found will it return true. The exponential time complexity of this method prohibits use for Sentences with many different atomic symbols.

Specified by:

isValid in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a tautology

isInconsistent

public boolean isInconsistent(Sentence stmt)

This function tests whether the given Sentence in propositional logic is inconsistent. A Sentence is inconsistent if and only if it is false under all possible Interpretations. This method loops over all possible Interpretations until it finds one that satisfies the given Sentence, in which case it returns false. Only if no such Interpretation can be found will it return true. The exponential time complexity of this method prohibits use for Sentences with many different atomic symbols.

Specified by:

isInconsistent in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a contradiction

getModel

public Interpretation getModel(Sentence stmt)

This function attempts to find a model for the given Sentence. A model is an Interpretation under which the Sentence evaluates to true. If such a model exists, the Sentence is satisfiable and the returned Interpretation proves this. If the Sentence is inconsistent then there is no model and this function returns null. This method enumerates all possible Interpretations and returns the first one it finds that satisfies the given Sentence.

Specified by:

getModel in interface TheoremProver

Parameters:

stmt - the Sentence for which a model is sought

Returns:

an Interpretation that satisfies the given Sentence, or null iff the Sentence is inconsistent

equivalent

public boolean equivalent(Sentence stmt1,
                          Sentence stmt2)

This function tests whether the two given Sentences are equivalent. Two Sentences are equivalent if they evaluate to the same truth value under all possible Interpretations.

Specified by:

equivalent in interface TheoremProver

Parameters:

stmt1 - the Sentence that may be equivalent to stmt2

stmt2 - the Sentence that may be equivalent to stmt1

Returns:

whether stmt1 and stmt2 are equivalent

follows

public boolean follows(Sentence stmt,
                       java.util.Collection<Sentence> axioms)

This function tests whether the given Sentence logically follows from the given Collection of Sentences.

Specified by:

follows in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

axioms - Sentences from which the axiom might follow

Returns:

whether stmt logically follows from axioms