Before initialisation, the tableau system is read into this structure.

A constraint is placed on a tableau rule to restrict the values to which its variables can be bound. This means that some applications of the rule will be blocked; but also that any "free" or "generative" variables (that is, variables that occur in the rule's productions but not in its consumptions) can now be associated with a set of possible assignments, thereby making it possible to, essentially, generate a choice of multiple instantiations of a single rule.

Indicates how to handle the situation where multiple rule instantiations are applicable to the same formula.

Due to their computational complexity, rules that do not take any consumptions are handled greedily regardless of the value of the compositor.

A rule describes which formulas it consumes and which it produces. In its basic form, it can represent both instantiated and uninstantiated tableau rules (see RuleInstantiated and RuleUninstantiated).

Before instantiation, a generator is described by a constraint. This constraint can only refer to static terms.

Represent sets of primitive source formulas to be used in restrictive constraints.

Represent sets of primitive source formulas to be used in generators and restrictive constraints.

Represent complex sets of source terms, to be turned into concrete terms at a point where it is known what they should refer to. Static terms are known at the start of the tableau procedure, whereas dynamic terms should be evaluated dynamically.

Shorthand for a specification of complex dynamic terms.

Shorthand for a specification of complex static terms.

Decide the validity of the target formula within the given logical system. A branch closes when it internally contradicts. A branch that is neither closed nor expandable corresponds to a satisfying assignment of the negation of the target formula, and constitutes a counter-model. Otherwise, we have successfully shown the formula's validity and can return a Tableau.

Construct the initial branch and settings for the decision algorithm.

The global state of the tableau — settings that will remain static after initialisation.

Relates values to their identifiers.

A Branch keeps track of the leaf of a single branch of the tableau, and all that came before.

Formulas on the branch are decorated by their reference number and marks.

After instantiation, a generator consists of all variable assignments that it allows.

Like Either, but remembers the original input in the Right case, too.

A proof in a tableau system is a rose tree, containing sets of formulas and the rule applications used to obtain them.

Eliminate rule applications that do not produce any formulas that are involved in closing any branch.

Note that this will not eliminate all unnecessary applications (let alone find the shortest proof) — it will only remove rules that are not involved in any closure. For example, for justification logic, if c:φ and d:ψ are in the CS but only d:ψ has to be introduced via CSr, then this will remove any redundant CSr application — but if a formula is introduced via a restricted cut, it could do nothing because the cut-formula IS involved in the closure of a branch, even though it was pointless to do the cut in the first place. It would be nice to think of a stronger method.

Make the reference numbers on the formulas heterogeneous, even if they are on different branches. This is done in a single step at the end so that we do not have the mental (and computational) burden of carrying a State monad everywhere.

If the root formula is not exactly equal to the input formula, there was supposedly a rewriting step. Add this step to the tableau explicitly, to show what happened.

Take the first option from a list of options.

Take the intersection of all given lists.

A variation on permutations: given a list that describes the possible elements at each position, give all possible element combinations. In a sense, this is a transpose operation.

Example: [[1,2],[3,4]] -> [[1,3],[1,4],[2,3],[2,4]]