Types
PropLogicFormula = ref object case of PropFormulaType.atomicProp: of PropFormulaType.andProp, PropFormulaType.orProp: left*, right*: PropLogicFormula of PropFormulaType.notProp: formula*: PropLogicFormula of PropFormulaType.impliesProp: antecedent*, consequent*: PropLogicFormula
- Object corresponds to logical formulae. This object uses a private field to express form (atomic formula, φ∧ψ, φ∨ψ, φ⇒ψ, or ¬φ) of the logical formula the instance represents.
Procs
proc `!`(formula: PropLogicFormula): PropLogicFormula {....raises: [], tags: [], forbids: [].}
-
Logical connective not. It is recommended to specify connection order with parentheses.
Example:
let P = generateAtomicProp() formula = !(!P) ## This is not (not P)
proc `$`(formula: PropLogicFormula): string {....raises: [ValueError, Exception], tags: [RootEffect], forbids: [].}
- Stringify procedure for PropLogicFormula.
proc `&`(left, right: PropLogicFormula): PropLogicFormula {....raises: [], tags: [], forbids: [].}
-
Logical connective and. It is recommended to specify connection order with paren.
Example:
let P = generateAtomicProp() Q = generateAtomicProp() R = generateAtomicProp() formula = (P & Q) & R ## This is (P and Q) and R
proc `==`(left, right: PropLogicFormula): bool {....raises: [], tags: [], forbids: [].}
-
Compare two logical formulae. This procedure determines == recursively.
Example:
let P = generateAtomicProp() Q = generateAtomicProp() assert (P & Q) == (P & Q) assert not ((P & Q) == (Q & P)) ## Note that (P and Q) and (Q and P) are treated as different formulae.
proc `=>`(antecedent, consequent: PropLogicFormula): PropLogicFormula {. ...raises: [], tags: [], forbids: [].}
-
Logical connective implies. It is recommended to specify connection order with parentheses.
Example:
let P = generateAtomicProp() Q = generateAtomicProp() R = generateAtomicProp() formula = P => (Q => R) ## This is P implies (Q implies R)
proc generateAtomicProp(): PropLogicFormula {....raises: [], tags: [], forbids: [].}
- Generate an atomic proposition.
proc generateAtomicPropWithGivenId(id: int): PropLogicFormula {....raises: [], tags: [], forbids: [].}
-
Returns atomic propositions with given id. If the atomic propositions which id is given id does not exist, this proc raises AssertionDefect.
This procedure is defined to generate new PropLogicFormula objects correspond to an existing atomic proposition. Use proc `generateAtomicProp` to generate new atomic propositions.
Example:
import propositionalLogic let P = generateAtomicProp() Q = generateAtomicPropWithGivenId(P.getId()) echo P == Q ## Output: ## true
proc getId(formula: PropLogicFormula): int {....raises: [], tags: [], forbids: [].}
- Get id of given atomic proposition. If formula is not atomic proposition, this procedure raises AssertionDefect.
proc getNumberOfAtomicProps(): int {....raises: [], tags: [], forbids: [].}
-
Example:
import propositionalLogic let _ = generateAtomicProp() _ = generateAtomicProp() assert getNumberOfAtomicProps() == 2
Returns number of atomic propositions. proc recByStructure[T](formula: PropLogicFormula; atomicCase: proc (formula: PropLogicFormula): T; andCase, orCase: proc (left, right: T): T; impliesCase: proc (antecedent, consequent: T): T; notCase: proc (val: T): T): T
- Get value of type T with recursion according to given formula's structure. The proc eval is an example of how to use this proc.
proc `|`(left, right: PropLogicFormula): PropLogicFormula {....raises: [], tags: [], forbids: [].}
-
Logical connective or. It is recommended to specify connection order with paren.
Example:
let P = generateAtomicProp() Q = generateAtomicProp() R = generateAtomicProp() formula = (P | Q) | R ## This is (P or Q) or R