|
|||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||
| Interface Summary | |
|---|---|
| ICNFFormula | A formula in conjunctive normal form |
| IConstant | |
| IFormula | Formula := P(Term, ....) | NOT(Formula) | Formula CONNECTIVE Formula | QUANTIFIER Formula | TRUE | FALSE |
| IFunction | An n-ary function |
| ILogicConstants | Constants used to build up formulae |
| ILogicDecorator | |
| IMaxTerm | A maxterm is a sum (disjunction) of atomic formulae (constants, relations, or quantified). |
| IRelation | an n-ary relational predicate symbol |
| ISemiDecisionProcedure | |
| ITerm | Term := Constant | Variable | f(Term,...) |
| ITheory | A theory is a set of sentences |
| IVocabulary<T extends IConstant> | Vocabulary of a calculus |
| Class Summary | |
|---|---|
| AbstractBinaryFormula | |
| AbstractConstant | |
| AbstractNumberedVariable | A term that represents a variable in a formula |
| AbstractSemiDecisionProcedure | Abstract base class for decision procedures. |
| AbstractTerm | |
| AbstractTheory | |
| AbstractVariable | A term that represents a variable in a formula |
| AbstractVocabulary<T extends IConstant> | |
| AdHocSemiDecisionProcedure | Ad-hoc decision logic. |
| BasicTheory | |
| BasicVocabulary<T extends IConstant> | A simple class to define a simple vocabulary of functions and relations |
| BinaryFormula | |
| BinaryFunction | |
| BinaryRelation | |
| BooleanConstant | |
| BooleanConstantFormula | |
| CNFFormula | A formula in conjunctive normal form. |
| CombinedTheory | The union of two theories. |
| CombinedVocabulary | |
| DefaultDecorator | |
| Disjunction | A disjunction of formulae |
| DoubleConstant | |
| EmptyTheory | |
| FloatConstant | |
| FunctionTerm | |
| IntConstant | |
| IntVariable | A term that represents an unconstrained integer variable in a formula |
| LongConstant | |
| NaryFunction | |
| NotFormula | A formula of the form not(f) |
| NotFormulaMaxTerm | An irreducible Not Formula. |
| NullaryFunction | a function that takes no parameters. |
| NumberConstant | |
| QuantifiedFormula | |
| RealNumberVariable | A term that represents an unconstrained real number variable in a formula |
| RelationFormula | An atomic formula of the form R(Term, ... |
| Simplifier | Utilities for simplifying logic expressions |
| UnaryFunction | |
| UnaryRelation | |
| Wildcard | A special constant used for pattern matching during substitution. |
| Enum Summary | |
|---|---|
| IFormula.Kind | |
| ILogicConstants.BinaryConnective | |
| ILogicConstants.Quantifier | |
| ITerm.Kind | |
|
|||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||