Procs
proc getModels(formula: PropLogicFormula): seq[Interpretation] {. ...raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns all models to the given formula. Be careful of computational complexity.
proc iff(left, right: PropLogicFormula): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
-
Returns true if left and right are logical equivalent, i.e. both left => right and right => left are tautology, and returns false otherwise.
Example:
import propositionalLogic let p = generateAtomicProp() q = generateAtomicProp() formula1 = p => q formula2 = !p | q assert formula1.iff(formula2)
proc isContradiction(formula: PropLogicFormula): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if given the formula contradicts and false otherwise. Be careful of computational complexity.
proc isContradiction(theory: seq[PropLogicFormula]): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if the given theory contradicts and false otherwise. Be careful of computational complexity.
proc isSat(formula: PropLogicFormula): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if the given formula is satisfiable and false otherwise. Be careful of computational complexity.
proc isSat(formula: PropLogicFormula; interpretation: Interpretation): bool {. ...raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if the given formula is true under the given interpretation and false otherwise.
proc isSat(theory: seq[PropLogicFormula]): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if the given theory is satisfiable (i.e. all formulae included in the given theory are satisfiable by the same interpretation) and false otherwise. Be careful of computational complexity.
proc isSat(theory: seq[PropLogicFormula]; interpretation: Interpretation): bool {. ...raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if all formulae included in the given theory becomes true under the given interpretation and false otherwise.
proc isTautology(formula: PropLogicFormula): bool {....raises: [Exception], tags: [RootEffect], forbids: [].}
- Returns true if the given formula is tautology and false otherwise. Be careful of computational complexity.