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.

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.

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.

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.

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.

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.

The concept of variable capture in a quantifier (or, more generically, in a BindingExpression) is a well-known one, and is also documented in functions such as this one. But Declarations function similarly to bindings, except their scope spans multiple expressions in the same (or inner) environments. So we can consider a secondary type of symbol capture, one in which we substitute into an expression $E$ in the scope of a declaration $D$, and doing so inserts an instance of a symbol $s$ that is free in $E$ but is declared by $D$. This function checks to see whether that would happen if we applied an instantiation to a formula.

For example, if we create a formula from the putdown notation { :[x] (+ a 1) }, with both x and a as metavariables, we could imagine an instantiation of a with the expression (* x 2). No capture would occur from the point of view of binding expressions, but capture would occur from the point of view of the declaration of x at the start of the environment, which functions conceptually like a binding. This function would return true in such a case, because capture of this type would occur.

Note that this function does not report on capture of the other type. That is, it may be the case that, for some expression E inside the formula, if we asked E.isFreeToReplace(a,b) where b is (* x 2), we would get false, but this function returns true, because it's not checking for capture inside of expressions by a BindingExpression, but rather it is checking only for capture that happens due to a declaration.

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.

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.