Lurch Deductive Engine

Class

PropositionalForm

Any LogicConcept can be interpreted as a proposition, in the usual sense of propositional logic, as follows.

  • An Expression (no matter how complex) is treated as atomic, and considered equal only to another expression with the exact same structure.
  • An Environment containing no children is treated as the constant "true."
  • An Environment containing exactly one child is treated the same as if it were just the child alone.
  • An Environment containing two claim children is treated as the conjunction of those children, after viewing each as a proposition itself.
  • An Environment containing a given $G$ followed by a claim $C$ is treated as the conditional expression "$G$ implies $C$."
  • An Environment with more than two children, $C_1$ through $C_n$, is viewed as if it contained only two children, first $C_1$ and then an environment containing $C_2$ through $C_n$.

For example, if we use putdown notation to express environments and expressions, then the LogicConcept written as

{
    :(> x 5)
    (> y 10)
    (= z 15)
}

might correspond to the proposition $P\Rightarrow(Q\wedge R)$, if $P$, $Q$, and $R$ were the propositional letters for the three expressions, in that order.

This conversion preserves the intended meaning of the notions of Environment and given/claim. Although LogicConcepts can be more complex than that (including declared variables, quantifiers, etc.), there are ways to reduce that complexity to propositional form. Once a LogicConcept is in propositional form, it can be checked using a propositional tautology checker, either intuitionistic or classical.

We will later add the preprocessing steps that can simplify variable and constant declarations down into content amenable to propositional checking. Those tools are not yet present in this version of the class.

Constructor

new PropositionalForm()

Source

Classes

PropositionalForm

Methods

static

atomic(LC, catalogopt) → {PropositionalForm}

Construct a new instance of the PropositionalForm class, an atomic one representing the given LogicConcept. Note that this is not a member function, but a static method, so you would invoke it using PropositionalForm.atomic(L,c). In fact, one does not ever construct instances of the PropositionalForm class in any way other than using the static methods of this class that create specific types of PropositionalForms.

Note that every LogicConcept gets represented by a different propositional letter. The internal structure of the LogicConcept is completely lost in this conversion. The second parameter is for internal use, to ensure that the same LogicConcept gets converted the same way each time.

Parameters

  • LC LogicConcept

    the LogicConcept to represent in propositional form

  • catalog Array <optional>

    a list of the text representations of previous LogicConcept instances that have been converted to PropositionalForm, so that later conversions of structurally identical LogicConcepts get the same results; this parameter is primarily used internally, and clients may omit it

See

Returns

  • PropositionalForm

    a PropositionalForm object representing the given LogicConcept LC

Source

static

conditional(antecedent, consequent, catalogopt) → {PropositionalForm}

Construct a new instance of the PropositionalForm class, a compound one representing a conditional expression, that is, one of the form $A\to B$, where $A$ is called the "antecedent" and $B$ the "consequent." Note that this is not a member function, but a static method, so you would invoke it using PropositionalForm.conditional(A,C,c). In fact, one does not ever construct instances of the PropositionalForm class in any way other than using the static methods of this class that create specific types of PropositionalForms.

The third parameter is for internal use, to ensure that atomic LogicConcepts gets represented consistently.

Parameters

  • antecedent LogicConcept

    the LogicConcept to use for the left-hand side of the conditional

  • consequent LogicConcept

    the LogicConcept to use for the right-hand side of the conditional

  • catalog Array <optional>

    this parameter is passed recursively to inner construction methods, so that eventually it can be used as documented in atomic()

See

Returns

  • PropositionalForm

    a PropositionalForm object representing the conditional expression described above

Source

static

constantTrue() → {PropositionalForm}

Construct a new instance of the PropositionalForm class, an atomic one representing the logical constant "true." Note that this is not a member function, but a static method, so you would invoke it using PropositionalForm.constantTrue(). In fact, one does not ever construct instances of the PropositionalForm class in any way other than using the static methods of this class that create specific types of PropositionalForms.

See

Returns

  • PropositionalForm

    a PropositionalForm object representing the logical constant "true"

Source

static

fromConclusion(conclusion, ancestoropt, catalogopt) → {PropositionalForm}

Build a PropositionalForm instance representing the sequent for a given conclusion. Recall that the notion of a "conclusion" within an Environment is documented here and also here. The sequent for a conclusion is a conditional $P_1\to\cdots\to P_n\to C$, whose meaning is like that of the sequent $P_1,\ldots,P_n\vdash C$, where $C$ is the conclusion and $P_1,\ldots,P_n$ are its accessibles.

Parameters

  • conclusion LogicConcept

    a conclusion inside a larger Environment, the sequent for which should be represented as a PropositionalForm instance

  • ancestor Environment <optional>

    the outer Environment in which to do the computation (i.e., no accessibles outside this Environment will be included)

  • catalog Array <optional>

    this parameter functions the same way that it does in atomic() and conditional(); clients rarely need to use it.

Returns

  • PropositionalForm

    a PropositionalForm instance representing the sequent whose conclusion is given as the first parameter and whose premises are the accessibles to that conclusion, within the given ancestor

Source

static

fromConclusionsIn(environment, catalogopt) → {Array.<PropositionalForm>}

This function simply repeats the work of fromConclusion() multiple times, once for each conclusion appearing in the given Environment, using that environment for the context in each case. The result is thus an array of the results one would get by running the loop.

One can view the conjunction of these PropositionalForm results as the meaning of the given Environment.

Parameters

Returns

  • Array.<PropositionalForm>

    an array of PropositionalForm instances, one for each conclusion in the given Environment, each one representing the sequent for that conclusion in that Environment

Source

static

sequent(…args) → {PropositionalForm}

Construct a new instance of the PropositionalForm class, a compound one representing a sequent, that is, one of the form $P_1,\ldots,P_n\vdash C$, for some list of premises $P_i$ and conclusion $C$. This is not actually a new type of compound expression different from a conditional(); it is simply a convenience function that will build nested conditionals to express the sequent in question. If each $P_i$ were an Expression, the sequent is equivalent to $P_1\to(P_2\to\cdots\to(P_n\to C)\cdots)$, but for more complex $P_i$, some conversion/factoring takes place to represent the final result as only nested conditionals.

Parameters

  • args any <repeatable>

    a sequence of LogicConcept instances representing the contents $P_1,\ldots,P_n,C$ of the sequent. Optionally, an additional last argument may be a catalog, which functions the same as it does in both atomic() and conditional(); clients rarely need to use it.

Returns

  • PropositionalForm

    a PropositionalForm instance representing the sequent, as documented above

Source

CNF() → {Array.<Array>}

The representation of this PropositionalForm object in conjunctive normal form, and thus ready for use in satisfiability checking. This function can be called by clients, but it is more likely to be called by them only indirectly, when they call isAClassicalTautology() or isAnIntuitionisticTautology().

See

Returns

  • Array.<Array>

    a representation of this PropositionalForm object in conjunctive normal form, as documented in the CNF namespace

Source

isAClassicalTautology() → {boolean}

Whether a propositional logic expression is a classical tautology can be checked by the laborious but straightforward method of truth tables. Such a method, however, is exponential in running time. So instead, we ask whether the negation of the expression is satisfiable, an equivalent question, but one that is amenable to the efficiencies in the satisfiability checker documented here.

See

Returns

  • boolean

    whether this PropositionalForm object is (when interpreted as a propositional logic expression) a tautology, using the rules of classical propositional logic

Source

isAnIntuitionisticTautology() → {boolean}

Whether a propositional logic expression is an intuitionistic tautology can be checked by attempting to construct a proof. Because we are limiting ourselves to expressions that contain only the conditional operator, there are only three possible logical rules in play, making the proof search a straightforward one. In the worst case scenario, the search still takes exponential time, but we incorporate a number of efficienceies into the search process to minimize that problem.

See

Returns

  • boolean

    whether this PropositionalForm object is (when interpreted as a propositional logic expression) a tautology, using the rules of intuitionistic propositional logic

Source

isConditional() → {boolean}

Check whether this instance of the PropositionalForm class is a conditional expression. Note that the only non-atomic form supported by this class is a conditional expression, because we need to support only sequents whose conclusion is an Expression, and (for detailed reasons not discussed here) such sequents can be expressed as nested conditional PropositionalForm instances.

See

Returns

  • boolean

    whether this instance is a conditional; note that this is true iff isAtomic() is false

Source

isConstantTrue() → {boolean}

Check whether this instance of the PropositionalForm class is an atomic one representing the logical constant "true." You can create such an instance using the static member function constantTrue(). Note that if this function returns true, then isAtomic() will also return true.

See

Returns

  • boolean

    whether this instance represents the constant "true"

Source

negatedCNF() → {Array.<Array>}

The representation of the negation of this PropositionalForm object in conjunctive normal form, and thus ready for use in satisfiability checking. This function can be called by clients, but it is more likely to be called by them only indirectly, when they call isAClassicalTautology() or isAnIntuitionisticTautology().

Note: Negating a CNF once created is a bothersome process, so it is much easier at the outset to have a routine that simply creates a CNF of the negation of the expression desired. That is the motivation for the creation of this method.

See

Returns

  • Array.<Array>

    a representation of the negation of this PropositionalForm object in conjunctive normal form, as documented in the CNF namespace

Source