Lurch Deductive Engine

Namespace

Formula

A formula is a LogicConcept that includes symbols intended to be used for substitution, that is, what the Matching module calls metavariables. This namespace provides functions for dealing with formulas, including converting a LogicConcept into a formula, computing the domain of a formula, and instantiating a formula.

Import this namespace with code such as import Formula from './formula.js' and then make calls such as Formula.domain( myLC ).

Members

staticconstant

cachedInstantiation

To facilitate marking some LogicConcepts as cached instantiations of formulas, we declare a string constant that can be used with the isA() and asA() and makeIntoA() functions in the MathConcept class.

This is used when we have a formula F and the inferences done in the scope of that formula cite the formula and create instantiations of it. Some of our algorithms then insert those instantiations as next siblings following F so that they are accessible at any location at which F is accessible. But in order to distinguish those algorithmically-created instantiations from content that was authored by the user, we mark algorithmically-created instantiations with an attribute. Specifically, for such an instantiation I, we would call I.makeIntoA( cachedInstantiation ), and can then test that later with I.isA( cachedInstantiation ).

See

Source

Methods

static

addCachedInstantiation(formula, instantiation)

As described in this documentation, we can insert after any formula instantiations of it. This function adds a new instantiation to that cache. It does not first check to be sure that the given instantiation is actually an instantiation of the given formula; the client is in charge of ensuring that. This function inserts the given instantiation at the end of the given formula's instantiation cache and also marks it with the appropriate attribute so that it can be clearly identified as part of the cache.

If the formula has no parent, it can have no siblings, and thus this function cannot do its job and will instead throw an error.

Parameters

  • formula LogicConcept

    add a cached instantiation of this formula

  • instantiation LogicConcept

    the instantiation to add to the cache

See

Source

static

allCachedInstantiations(formula) → {Array.<LogicConcept>}

As described in this documentation, we can insert after any formula instantiations of it. The sequence of next siblings after a formula that have been marked as instantiations of it (using this constant) are that formula's instantiation cache. This function returns that cache as a JavaScript array, in the same order that the siblings appear following the formula. It may have zero or more entries, but will always be an array.

If the given formula has no parent, it will have no siblings and thus no instantiation cache, and this function will return an empty array.

Parameters

  • formula LogicConcept

    the formula whose cache should be computed

See

Returns

  • Array.<LogicConcept>

    the array of instantiations cached for the given formula

Source

generatorstatic

allPossibleInstantiations(formula, candidate)

What are all instantiations of the given formula that produce the given candidate?

On the one hand, it may seem like this is a simple application of the Matching module, and this is somewhat true. The only additional feature provided here is that the formula and its candidate instantiation need not be Expressions. If they are not, then they must have isomorphic structure except for any Expressions inside the two, which will be paired up to construct a matching problem, whose solutions will be returned.

In other words, this function extends matching to support a single pair of inputs that do not need to be Expressions, and it does exactly what you'd expect in that case.

This function is a generator that yields zero or more ways to instantiation formula to produce candidate; all possible ways will be enumerated, though it may be that there are no such ways, in which case the enumeration will be empty.

Parameters

Source

static

clearCachedInstantiations(formula, instantiation)

As described in this documentation, we can insert after any formula instantiations of it. This function removes all entries from that cache. Because the cache is defined to be the sequence of siblings following the formula that have the appropriate attribute, this function actually removes those LogicConcepts from their parent (which is also the parent of the given formula).

If the given formula has no parent, it will have no instantiation cache, and so this function will do nothing.

Parameters

  • formula LogicConcept

    add a cached instantiation of this formula

  • instantiation LogicConcept

    the instantiation to add to the cache

See

Source

static

domain(formula) → {Set}

Once a LogicConcept has been converted into a formula, it will have zero or more metavariables. This function returns the set of names of those metavariables. If the formula has no metavariables, or if a non-formula LogicConcept was passed as input, this function will return the empty set.

Parameters

  • formula LogicConcept

    the LogicConcept to view as a formula, and whose metavariables should be investigated to compute this function's result

Returns

  • Set

    the set of names of Symbols in the given formula that appear as a metavariable therein

Source

static

from(LC, inPlaceopt) → {LogicConcept}

A LogicConcept can be converted into a formula by replacing any subset of its Symbols with metavariables. Recall that a metavariable can be any symbol, but with a specific attribute set to "true."

Which Symbols should be converted into metavariables? Any one that is not in the scope of a Declaration of that same Symbol. For example, if we consider the LogicConcept indicated by the putdown notation { :(= a b) (= b a) } and we assume it is in the scope of a Declaration of the = Symbol, but not of the a or b Symbols, then converting { :(= a b) (= b a) } to a formula would produce a copy in which each instance of a and b have had their metavariable attribute set to "true" (via a call to the makeIntoA() member).

The exception is that bound variables are never marked as metavariables.

Parameters

  • LC LogicConcept

    the LogicConcept to convert into a formula

  • inPlace boolean <optional>
     false

    if true, the metavariables will be attributed in LC itself, and the resulting modified LC is returned. If false, it will attribute and return a separate copy of LC, leaving the original unchanged.

Returns

  • LogicConcept

    a structural copy of LC, except with the relevant Symbol atoms converted into metavariables

Source

static

instantiate(formula, instantiation, preserve)

Instantiating a formula means making a copy of that formula and then replacing each metavariable in it with another LogicConcept, according to some predetermined mapping of metavariable names to LogicConcepts, called the "instantiation." This function performs exactly that operation, with two exceptions.

First, this function does not check to ensure that the domain of the given instantiation matches the domain of the given formula. If that is important to the caller, they should verify that themselves in advance, using an equality check between the two sets.

Second, this function also applies beta reduction to the result before returning it (if necessary) because the instantiation may have introduced an explicit expression function in a position where it should be applied to its arguments. Note the warnings in the beta reduction documentation about infinite loops.

Parameters

  • formula LogicConcept

    the LogicConcept to instantiate with the given instantiation

  • instantiation Substitution | Solution | Object | Map

    either a Substitution instance (which describes a single metavariable's replacement) or a Solution instance (which describes the substitution of zero or more metavariables) or a JavaScript Object or Map (which should map metavariable names to the desired instantiations) to be used as the function to apply to each metavariable in the formula

  • preserve Array.<String>

    the list of attributes to preserve while doing the instantiation. Any metavariable having these attributes will have the values of those attributes copied over to its instantiation. All other attributes of the metavariable (including, typically, the fact that it is a metavariable) will be lost during the instantiation. This defaults to the list containing just one entry, the "given" type attribute flag.

Source

generatorstatic

possibleSufficientInstantiations(sequent, formula, options)

Given a sequent and a formula, is there an instantiation of the formula that, if added as another premise to the sequent, would make the sequent true? The answer to that question depends upon which deductive system is providing the meaning of "true" for sequents, but in any reasonable case, finding exactly the set of instantiations that would make a sequent true will typically be at least as difficult as validating the instantiated sequent, perhaps moreso. Consequently, this function does not attempt to find the exact correct answer to that question, but rather finds a superset of the answer, guaranteeing that any instantiation that would make the sequent hold will be among the results. Those results can be filtered further, if desired, by the client, by running them through the validation algorithm for the deductive system in play.

The default is to search for instantiations that will make the sequent true when validated by classical propositional logic. However, if the client will be using intuitionistic propositional logic instead, the results can be filterted further; simply set intuitionistic: true in the options object. This will not only return fewer results, but also speed up the search for those results.

The default is to search for instantiations that will make the sequent true even if the formula itself is only an intermediate step in a larger chain of inferences. However, it is often the case that the client wants the formula to be the final step that achieves the sequent's conclusion (say, if a student should be expected to cite a formula directly relevant to the statement they're justifying). This will significantly narrow the search space and the result set and will consequently speed up the search. Simply set direct: true in the options object.

The default is to do the work silently, not generating any debugging output. But if debugging a complex problem, it may help to see the inner workings of this function. Set debug: true in the options object to print copious debugging output to the console.

This function is a generator that yields a sequence of objects in the same format as those returned by allInstantiations(); see its documentation for details.

Parameters

  • sequent Sequent

    the sequent whose conclusion the client hopes to justify by instantiating the formula

  • formula Formula

    the formula whose possible instantiations are to be explored

  • options Object

    a dictionary of options, which default to { direct: false, intuitionistic: false, debug: false } and whose meaning is given above

Source