Index

Modules: propositionalLogic, propositionalLogic/constants, propositionalLogic/evalUtils, propositionalLogic/formulae, propositionalLogic/hashUtils, propositionalLogic/interpretationUtils, propositionalLogic/parse, propositionalLogic/simplification, propositionalLogic/truthValue.

API symbols

`!`:

• formulae: proc `!`(formula: PropLogicFormula): PropLogicFormula

`$`:

• formulae: proc `$`(formula: PropLogicFormula): string
• truthValue: proc `$`(val: TruthValue): string

`&`:

• formulae: proc `&`(left, right: PropLogicFormula): PropLogicFormula

`==`:

• formulae: proc `==`(left, right: PropLogicFormula): bool
• truthValue: proc `==`(left, right: TruthValue): bool

`=>`:

• formulae: proc `=>`(antecedent, consequent: PropLogicFormula): PropLogicFormula

`and`:

• truthValue: proc `and`(left, right: TruthValue): TruthValue

`not`:

• truthValue: proc `not`(val: TruthValue): TruthValue

`or`:

• truthValue: proc `or`(left, right: TruthValue): TruthValue

`|`:

• formulae: proc `|`(left, right: PropLogicFormula): PropLogicFormula

andSymbol:

• constants: const andSymbol

BOTTOM:

• truthValue: let BOTTOM

eval:

• interpretationUtils: proc eval(formula: PropLogicFormula; interpretation: Interpretation): TruthValue

generateAtomicProp:

• formulae: proc generateAtomicProp(): PropLogicFormula

generateAtomicPropWithGivenId:

• formulae: proc generateAtomicPropWithGivenId(id: int): PropLogicFormula

getId:

• formulae: proc getId(formula: PropLogicFormula): int

getModels:

• evalUtils: proc getModels(formula: PropLogicFormula): seq[Interpretation]

getNumberOfAtomicProps:

• formulae: proc getNumberOfAtomicProps(): int

getNumberOfInterpretations:

• interpretationUtils: proc getNumberOfInterpretations(): int

hash:

• hashUtils: proc hash(formula: PropLogicFormula): Hash
• hashUtils: proc hash(truthValue: TruthValue): Hash

iff:

• evalUtils: proc iff(left, right: PropLogicFormula): bool

impliesSymbol:

• constants: const impliesSymbol

Interpretation:

• interpretationUtils: type Interpretation

interpretations:

• interpretationUtils: iterator interpretations(): Interpretation

isContradiction:

• evalUtils: proc isContradiction(formula: PropLogicFormula): bool
• evalUtils: proc isContradiction(theory: seq[PropLogicFormula]): bool

isOperator:

• constants: proc isOperator(x: char): bool
• constants: proc isOperator(x: string): bool

isParen:

• constants: proc isParen(x: char): bool
• constants: proc isParen(x: string): bool

isSat:

• evalUtils: proc isSat(formula: PropLogicFormula): bool
• evalUtils: proc isSat(formula: PropLogicFormula; interpretation: Interpretation): bool
• evalUtils: proc isSat(theory: seq[PropLogicFormula]): bool
• evalUtils: proc isSat(theory: seq[PropLogicFormula]; interpretation: Interpretation): bool

isTautology:

• evalUtils: proc isTautology(formula: PropLogicFormula): bool

leftParen:

• constants: const leftParen

notSymbol:

• constants: const notSymbol

orSymbol:

• constants: const orSymbol

parse:

• parse: proc parse(formula: string; nameToAtomicFormulae: Table[string, PropLogicFormula]): ( PropLogicFormula, Table[string, PropLogicFormula])

PropLogicFormula:

• formulae: type PropLogicFormula

recByStructure:

• formulae: 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

rightParen:

• constants: const rightParen

simplification:

• simplification: proc simplification(formula: PropLogicFormula): PropLogicFormula

TOP:

• truthValue: let TOP

TruthValue:

• truthValue: type TruthValue