Types
Interpretation = Table[PropLogicFormula, TruthValue]
- Type alias represents interpretation. The keys are atomic propositions.
Procs
proc eval(formula: PropLogicFormula; interpretation: Interpretation): TruthValue {. ...raises: [Exception], tags: [RootEffect], forbids: [].}
-
Evaluate formula with interpretation, and returns TOP if the formula is true under the interpretation and BOTTOM otherwise.
Example:
import tables import propositionalLogic let P = generateAtomicProp() Q = generateAtomicProp() interpretation = { P: TOP, Q: BOTTOM }.toTable assert (P | Q).eval(interpretation) == TOP
proc getNumberOfInterpretations(): int {....raises: [], tags: [], forbids: [].}
-
Example:
import propositionalLogic let _ = generateAtomicProp() _ = generateAtomicProp() _ = generateAtomicProp() assert getNumberOfInterpretations() == 8
Returns number of interpretations.
Iterators
iterator interpretations(): Interpretation {....raises: [Exception], tags: [RootEffect], forbids: [].}
-
Iterator generates all interpretations to all atomic propositions. Be careful of computational complexity (O(N * 2^N) where N is the number of atomic propositions).
Example:
import propositionalLogic let P = generateAtomicProp() Q = generateAtomicProp() formula = P => (Q | !Q) for interpretation in interpretations(): assert formula.isSat(interpretation)
Note that to check whether a formula is a tautology, satisfiable, or a contradict, use proc isTautology, isSat, or isContradict respectively.