| AssociativePlFormula | 
 This class captures the common functionalities of formulas with an associative
 operation like conjunction, disjunction, etc. 
 | 
| Conjunction | 
 This class represents a conjunction in propositional logic. 
 | 
| Contradiction | 
 A contradictory formula. 
 | 
| Disjunction | 
 This class represents a disjunction in propositional logic. 
 | 
| Equivalence | 
 This class models equivalence of propositional logic. 
 | 
| Implication | 
 This class models the implication of propositional logic. 
 | 
| Negation | 
 This class models classical negation of propositional logic. 
 | 
| PlBeliefSet | 
 This class represents a knowledge base of propositional formulae. 
 | 
| PlFormula | 
 This class represents the common ancestor for propositional formulae. 
 | 
| PlPredicate | 
 A specialized predicate for propositional logic that only allows an identifier
 but has no arguments and therefore has an arity of zero. 
 | 
| PlSignature | 
 This class captures the signature of a specific propositional language. 
 | 
| Proposition | 
 This class represents a simple proposition in propositional logic. 
 | 
| SpecialFormula | 
 This class captures the common functionalities of the special
 formulas tautology and contradiction. 
 | 
| Tautology | 
 A tautological formula. 
 |