Class | Description |
---|---|
AssociativeFOLFormula |
This class captures the common functionalities first order associative formulas like conjunction,
disjunction, etc.
|
Conjunction |
The classical conjunction of first-order logic.
|
Contradiction |
A contradictory formula.
|
Disjunction |
The classical disjunction of first-order logic.
|
ExistsQuantifiedFormula | |
FOLAtom |
An atom in first-order logic, i.e.
|
FolFormula |
The common abstract class for formulas of first-order logic.
|
FolSignature |
This class captures the signature of a specific
first-order language.
|
ForallQuantifiedFormula |
For-All quantified formula.
|
LogicStructure |
This abstract class captures the common functionalities of both
formulas and terms.
|
Negation |
The classical negation of first-order logic.
|
QuantifiedFormula |
The common parent of exists and forall quantified formulas, which contains common
functionalities.
|
RelationalFormula |
This interface models a relational formula, i.e.
|
SpecialFormula |
This class captures the common functionalities of the special
formulas tautology and contradiction.
|
Tautology |
A tautological formula.
|