|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
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
).
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 |
---|
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.
stmt
- the Sentence to be tested
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.
stmt
- the Sentence to be tested
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.
stmt1
- the Sentence that may be equivalent to stmt2stmt2
- the Sentence that may be equivalent to stmt1
boolean follows(Sentence stmt, java.util.Collection<Sentence> axioms)
This function tests whether the given Sentence logically follows from the given Collection of Sentences.
stmt
- the Sentence to be testedaxioms
- Sentences from which the axiom might follow
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |