Lurch Deductive Engine

Class

CNFProp

Represents the Propositional Form of any LC and the utilities to convert that to cnf form required by satSolve. It is needed because the PropositionalForm class does not support LCs, only sequents.

Constructor

new CNFProp(op, …kids) → {CNFProp}

Create a new CNFProp object.

Parameters

  • op 'and' | 'or'

    The operator of the CNFProp. Either 'and' or 'or'.

  • kids CNFProp | integer <repeatable>

    The children of the CNFProp that the operator applies to. An array of CNFProps or integers.

Returns

  • CNFProp
    • The newly created CNFProp object.

Source

Classes

CNFProp

Members

static

switchVarSymbol

Represents the symbol used for displaying switch variables in Algebraic form. The switch variable symbol is currently '𝒵', which is represented by the unicode \u{1D4B5}.

Source

Methods

hasCNFform() → {boolean}

Check if the logical expression is in Conjunctive Normal Form (CNF).

Returns

  • boolean

    True if the expression is in CNF, false otherwise.

Source

simplify()

Distribute all negatives by DeMorgan's law, and cancel double negatives that result on this CNFProp. See the Propositional Form for details.

Source

toAlgebraic()

Convert a CNFProp to algebraic form. The optional argument n tells it the lower bound for switch variables. See the Propositional Form for details.

Source

toEnglish()

Convert this CNFProp to human readable form using the supplied catalog. See the Propositional Form for details.

Source

static

toCNF(Lprop, switchvar) → {CNFProp}

Convert this CNFProp to CNF form. Lprop should be a simplified CNFProp. switchvar is an object containing the value to use for the next switch var with key num, e.g. a typical use might be

CNFProp.toCNF(CNFProp.fromLC(L),{num:L.catalog().length})

Parameters

  • Lprop CNFProp

    Simplified CNFProp

  • switchvar number

    Object with key num whose values if the value to use for the next switchvar

Returns

  • CNFProp
    • CNF form of this CNFProp

Source

static

toVar(x, nopt) → {string}

Converts an integer $x$ to a variable. If the optional argument $n$ is present, return a switch variable if $n<\left|x\right|$.

Parameters

  • x number

    The integer to be converted.

  • n number <optional>

    An optional argument that indicates the value after which a switch variables should be returned.

Returns

  • string

    The variable name corresponding to the integer $x$.

Source