Semantic tableaux with free variables.
In the tableau of the module SemanticTableaux a universal formula (γ) is instantiated with closed terms, which have
to be guessed in advance. Here a γ formula is instantiated with a new free variable, and the variables get their
values when they are needed to close a branch: two literals close a branch when their atoms unify, and the unifier
is applied to the whole tableau (the variables are rigid: a variable has the same value in every branch). An
existential formula (δ) is instantiated with a Skolem term on the free variables of the formula (the δ⁺ rule): a new
constant if it has none.
In each branch the rules are applied in this order: double negations, α and δ formulas, then β formulas (first one with a component that closes a branch at once), then γ formulas (the least used one). A formula already in the branch is not added again, and a β formula with a component in the branch is not expanded.
The search for a closed tableau proves the branches from left to right. When a literal can close the branch in several ways, or can also be kept open (because the unifier would bind variables that another branch may need), each way is an alternative, and the search backtracks to the next one when a later branch cannot be closed. A closure that binds no variable, or only variables that no other open branch has, is never undone. The number of times that each γ formula can be used in a branch grows from 1 to a limit (iterative deepening), so that the simplest closed tableaux are found first.
The answer is one of three:
Closed: every branch is closed, so the set of formulas is unsatisfiable.Open: a branch is fully expanded and open, and has no γ formulas, so the set is satisfiable (its literals
define a Herbrand model).Unknown: no closed tableau was found within the limits. First-order satisfiability is undecidable, and a
branch with a γ formula (other than a vacuous one, like ∀x P(a)) is never fully expanded.Equality is only used to close branches with ¬(t = t) (after unification), and with complementary equalities: a
fully expanded open branch with an equality s = t between different terms gives Unknown. The module
SemanticTableauxEQ has rules for equality.
The free variables of the input formulas are universally quantified, as in the other tableaux and in resolution: the tableau starts from their universal closures.
A node of the tree: its number i (its depth in the branch; 0 for the leaves), its formula (with the free variables it was given), the
rule that produced it, the numbers of the nodes it comes from, and a substitution: the instantiation of the bound
variable for γ and δ, and the bindings of the free variables made to close the branch for a closure.
The rule that produced a node. Alpha and Beta carry the component (1 or 2). The leaves are Closure (closed
branch), OpenLeaf (fully expanded open branch), LimitLeaf (a branch stopped by the limits) and Unexplored (a
branch that the search did not reach).
The answer of the search. Unknown says which limits were reached, or that an open branch has equalities.
The limits of the search: the maximum number of uses of each γ formula in a branch (the iterative deepening goes from 1 to it), the maximum number of rule applications in a branch (at most 250, so that the tree can be drawn without overflowing the call stack of a browser), and the maximum number of steps of the search.
Limits suitable for the problems of a logic course: { gammaUses = 3, depth = 40, steps = 20000 }.
It builds a free-variable tableau of a set of formulas, with defaultLimits except for the maximum number of
uses of each γ formula in a branch and the maximum number of rule applications in a branch, which are given:
semanticTableauFV fs maxGammaUses maxDepth.
It builds a free-variable tableau of a set of formulas with the given limits.
It says if the tableau is closed, that is, if it proves that the set of formulas is unsatisfiable.
A sentence that explains the answer.
It represents the tableau as a string: a node per line, indented by its depth, with the rule that produced it,
and the answer at the end. Each formula is numbered by its depth in the branch: 5. ¬P(x₁) % β(4).
It represents the tableau as a DOT graph (GraphViz). The first node is the summary of the answer. Each formula
is numbered by its depth in the branch, and the edges show the rules: α(4), β(4), γ(1){x/x₁},
δ(3){y/ş₁(x₁)}, ¬¬(2); a closed branch ends in ✕, and the edge ⊥(3,6){x₁/a} names the two formulas that
close it and the bindings of the free variables that the closure makes. An open branch ends in ◯, one stopped by
the limits in ⓤ and one not explored in ….
A free-variable tableau: the tree, the answer, the substitution of the free variables, the limit on the uses of the γ formulas with which the answer was obtained, and the number of steps of the search.