ai.krr.fol
Interface TheoremProver

All Known Implementing Classes:
HerbrandGenerator

public interface TheoremProver

This interface represents a theorem prover for first-order 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 and Interpretation#falsifies).

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.
 boolean isInconsistent(Sentence stmt)
           This function tests whether the given Sentence in first-order logic is inconsistent.
 boolean isValid(Sentence stmt)
           This function tests whether the given Sentence in first-order logic is valid.
 

Method Detail

isValid

boolean isValid(Sentence stmt)

This function tests whether the given Sentence in first-order 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 first-order 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

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