ai.krr.propositions
Interface TheoremProver

All Known Implementing Classes:

DPSolverIE, InterpretationEnumerator, RTPSolverIE

public interface TheoremProver

This interface represents a theorem prover for propositional logic.

The functionality to test whether a Sentence is satisfied or falsified by an Interpretation is not provided here, but can be accessed through the Interpretation (see Interpretation.satisfies(ai.krr.propositions.Sentence) and Interpretation.falsifies(ai.krr.propositions.Sentence)). The function getModel(ai.krr.propositions.Sentence) can be used to find an Interpretation that satisfies a given Sentence.

Author:

Gerhard Wickler

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.

Method Detail

isValid

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.

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a tautology

isInconsistent

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.

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a contradiction

getModel

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.

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

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.

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

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

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

Parameters:

stmt - the Sentence to be tested

axioms - Sentences from which the axiom might follow

Returns:

whether stmt logically follows from axioms