| 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. | 
| EqualityPredicate | This class models an equality predicate, meaning 
 a predicate of arity 2 that maps to the identity relation. | 
| Equivalence | The equivalence of first-order logic. | 
| ExistsQuantifiedFormula | Exists-quantified first-order logic formula. | 
| FolAtom | An atom in first-order logic, i.e. | 
| FolBeliefSet | This class models a first-order knowledge base, 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 first-order logic formula. | 
| Implication | The implication of first-order logic. | 
| InequalityPredicate | This class models an inequality predicate, meaning 
 a predicate of arity 2 that maps to the complement of the identity relation. | 
| LogicStructure | This abstract class captures the common functionalities of both
 formulas and terms. | 
| Negation | The classical negation of first-order logic. | 
| SpecialFormula | This class captures the common functionalities of the special
 formulas tautology and contradiction. | 
| Tautology | A tautological formula. |