* Introduction

This is the source code for [[https://www.umsu.de/trees]], a website that implements
a tableau prover for classical propositional and predicate logic, as well as
some modal logics. The prover is written in Javascript and runs entirely in the
browser.

* Development tools

** Run locally

The ~index.php~ file that serves the prover contains a few lines of php for
turning debugging features on/off. You can run the page locally by renaming
~index.php~ to ~index.html~ and opening it with your browser. The debugging
features won't work this way. To use them, you need to install php. Then run

#+BEGIN_SRC bash
php -S localhost:1234 router.php
#+END_SRC

and visit ~localhost:1234~.

** Debugging information

Add ~?debug=1~ to the URL to get a detailed log of what the script is doing.

** Tests

A few tests can be called in the browser at ~tests.html~.

There's also ~testdrive.php~, which registers how fast the prover is at processing
a sample of (valid and invalid) input formulas. This is useful for checking if a
change leads to a significant speedup or slowdown or even to inaccurate
classifications as valid or invalid. (PHP required.)

* Overview

Textbook tableau rules are inefficient for automated proving. Behind
the scenes, we therefore use somewhat different rules. Once a closed tableau is
found, we translate it back into the textbook rules to display on the page.

** Free variables, unification, and run-time skolemization

A major problem for automated proving is to figure out which term to use when
instantiating "gamma" formulas (of type ∀xA or ¬∃xA). Blindly trying all
possibilities is inefficient. A useful trick is to use "free-variable" tableaux
in which gamma formulas are initially expanded with dummy variables.

For example, in a free-variable tableau, we would expand ∀xFx as Fy, with y
free. Whenever a new formula is added, we then check if some substitution of
terms for the free variables (= some *unification*) would close the branch. For
example, if the branch contains ¬Fc, we can substitute c for y and close the
branch. (Even in a free-variable tableau, gamma nodes may need to be expanded
more than once.)

A problem now arises for the expansion of "delta" nodes (∃xA or ¬∀xA). Suppose
we've expanded Gamma(x) to Gamma(y). When expanding Delta(x), we want the
instance term to be new, no matter what we later substitute for y. To secure
this, we use *run-time skolemization*: we use f(y,...) as the new term for the
delta expansion, where f is a new function symbol and y,... are all free
variables on the branch.

(It would actually suffice to use only the free variables in Delta(x), but that
makes conversion into textbook sentence tableaux hard.)

** Negation normal form

A common trick in automated reasoning with tableaux is to convert the starting
formulas into some normal form that is easier to work with. [[https://en.wikipedia.org/wiki/Conjunctive_normal_form][Clausal normal form]]
is a popular choice, but again it makes back-conversion into textbook tableaux
difficult. We instead use [[https://en.wikipedia.org/wiki/Negation_normal_form][negation normal form]]. That is, the boolean operators
are reduced to conjunction, disjunction, and negation, and negation is only
applied to boolean atoms. 

On reflection, I am not sure how much this helps to speed things up. It slightly
simplifies the behind-the-scenes proof search, because we don't need rules for
expanding biconditionals etc., but it adds a layer of complexity to the code,
due to the back-and-forth translation between behind-the-scenes formulas and
displayed formulas, where we need e.g. the biconditional expansion rule after
all.

** Identity (Equality)

I describe my approach to handling identity in [[https://www.umsu.de/blog/2021/722][this blog post]].

** Translation of modal formulas

Modal input formulas are converted (by the "standard translation") into formulas
of (two-sorted) predicate logic, so that the behind-the-scenes prover only works
with predicate logic formulas.

Unfortunately, there are a few complications.

For one, the standard tableau rules applied to translated modal formulas easily
create tableaux that are hard to convert back into textbook modal tableaux. For
example, □A is translated into ∀x(¬wRx v Ax); by the standard free-variable rule
for gamma expansions, this would be expanded to ¬wRy ∨ Ay, which in turn is
expanded into two sub-branches. By the textbook rules, however, □A at w can only
be expanded if we already have another node of form wR*. Moreover, expanding □A
does not involve any kind of branching. 

We could require that the expansion of ¬wRy ∨ Ay is only allowed if the ¬wRy
subbranch immediately closes because it can be unified with some wR* node
earlier on the branch. That would make the resulting tableau relatively easy to
convert back into a textbook tableau. But then we might as well use a special
rule for expanding ∀x(¬wRx v Ax), which mimics the standard rule for □A: expand
directly to A*, but only if wR* is already on the branch.

This is the rule I currently use. Its downside is that it doesn't make use of
free variables at all: ∀x(¬wRx v Ax) is instantiated with a term * that already
occurs in a wR* node; so we immediately unify the instance variable with an
existing term. (Having no free variables for worlds, we also don't need skolem
terms for worlds in delta expansions.)

A second complication arises from constraints on the accessibility relation. In
textbook tableaux, these correspond to special rules for expanding tableaux. We
could instead translate the constraints into quantified formulas and add them to
the starting formulas for the tableau construction. But again that would often
lead to tableaux that don't look like textbook tableaux; for example, expanding
the transitivity node would lead to a two-fold branching. So the
behind-the-scenes prover now has special accessibility rules mimicking the
textbook rules.

All this makes it doubtful that much is gained by translating modal formulas
into predicate-logic formulas. As in the case of negation normal form, the
translation adds a layer of complexity to the code that should earn its keep.

On the other hand, the complications do not arise for the simplified tableau
rules of S5, where we can ignore the accessibility clauses. Here we use the full
free-variables machinery. The translation also simplifies the "model finder"
(see below).

[Here's a starting point for making use of free variables: if ∀x(wRx → px) and
any wR* occurs on a branch, append px. If the branch also contains ¬pv, it can
be closed. When closing the branch, we must take into account not only that it
contains px and ¬pv, but also (i) that it contains wRv, and (ii) that px was
expanded from w. So before we unify px and ¬pv, we would need to check that v is
a "legitimate value" of x. Legitimate values are any names * for which wR* is on
the branch. To find the legitimate values, we could note that px is derived
from ∀x(wRx → px), which figures 'w' in the crucial place, meaning that we need
substitutions whose value satisfies wR*.)

As it stands, this is too simple. Suppose we have a node ∀y(xRy → py), from an
expansion of □□p at w, with free x. We also have wRv, vRu, and ¬pu. We want to
expand ∀y(xRy → py) to py and unify y with u. So the rule for expanding box
formulas ∀y(xRy → py) must allow expanding to y whenever some ^R* is on the
tree, where ^ is a legitimate value of x. This needs more thought and/or
research.]

** The Modelfinder

Often there are simple countermodels that are hard to find through the tableau
method. We therefore run a separate algorithm to find smallest countermodels.

In outline, this works as follows.

1. We transform the formulas for which we want to find a model into clausal
   normal form, which gives us literal "constraints" that we're trying to
   satisfy. For example, Fa ∧ Fb is split into two constraints, Fa and Fb;
   ∀x∃yRxy is turned into Rxf(x); Fa ∨ Fb is turned into the disjunctive
   constraint [Fa, Fb].

2. Now we start with a domain of size 1, namely {0}. If no countermodel is
   found, we increase the domain to {0,1}, and so on. The interpretation of
   terms and predicates is initially empty. For each domain choice, we do the
   following:

3. We replace free variables in the constraints by numbers. So for domain [0,1],
   Fx would replaced by two constraints, F0 and F1. [Numerals in formulas are
   never interpreted as terms, so there can be no clash.]

4. We now iterate over all possible interpretations of the predicates and
   function expressions. For each expression, we first record the clauses
   that contain it. Then we enter this loop:

   a. Take the first/next uninterpreted expression.
   b. For each possible interpretation of that expression:
      i. Substitute that interpretation into the clauses.
      ii. Simplify the new clauses.
      iii. If the new clauses contain an empty clause, the interpretation
           is not a model; try the next.
      iii. If the new clauses force the interpretation of any other
           expression, update the interpretation and repeat from i.
   c. If no interpretation of the expression worked, backtrack.

Models for originally modal formulas have two domains, W and D. The elements of
W are also natural numbers starting with 0. Accessibility conditions like
reflexivity are added to the formulas for which we want to find a model.

* Copyright

Copyright © 2001-2026 Wolfgang Schwarz (wo@umsu.de)

You may use, distribute and modify this code under the terms of the GPLv3
license; see LICENSE.