Logical calculation with Tableaux

The Tableaux is a logical calculus tool that is very useful to demonstrate a conclusion from a set of premises, find counterexamples or models of a set of logical formulas or demonstrate that a formula is a tautology, i.e., that is true in all possible cases. They can be used in artificial intelligence as the basis for implementing automated theorem proving.

Although the Tableaux can be used with multiple logical systems, in this article, for simplicity, I will only apply it to predicate logic.

In this link you can download the Tableaux project whit an example of implementation, written in CSharp with Visual Studio 2013.

The program looks like this:

In the Premises and Conclusion text editors you can write formulas of predicate logic using the following connectives: ! for negation, & for conjunction (logical AND), | for disjunction (logical OR) -> for the implication and <-> for the double implication, although the latter two will be converted internally in formulas composed exclusively of negations, conjunctions and disjunctions:

A -> B becomes !A | B, and A <-> B becomes (!A | B) & (!B | A).

The classes used to compile and manage the formulas are in the Formulas folder of the Tableaux project, and are based on the design of the parser of the article design of the grammar for an expressions analyser.

The operator with the highest precedence is the negation, followed by implication and double implication, and finally, the conjunction and disjunction. You can use parentheses to change the precedence rules.

The procedure used by the Tableaux is very simple. It starts of the set of premises, which are written each one on a line in the Premises text editor, and the conclusion negated, since the Tableaux attempts to refute that the conclusion follows from the premises (or that the conclusion is not a contradiction, if there is no premises).

These formulas are the initial branch of the Tableaux. From here you can perform two type of operations, with conjunctive formulas (which can be written as two sub formulae linked together by the & connective) or disjunctive ones (ditto, with the | connective).

At each step, an appropriate formula from anywhere in the Tableaux is selected. Conjunctive formulas are divided into those two at the sides of the connective, and they are added at the end of the current branch. This operation can only be done if in the branch does not already appear none of the sub formulae, looking from the tree root to the end of this sub-branch.

With the disjunctive formulas, the current branch is divided in two sub-branches, each one starting with one of the sub formulae at the two sides of the connective. The same rule as in the previous case is applied: none of the sub formulae can be already present in the sub-branch.

When a formula and its negation appears in a branch, this branch is considered closed and it can no longer be used to expand the Tableaux.

This process is repeated until no more operations can be performed. At this time, the Tableaux is finished. If all its branches are closed, it is considered proven the conclusion from the premises, otherwise, the conclusion does not follow from the premises, and we can get counterexamples from the branches that are open. The propositions that are not part of a formula and appear negated in those branches are considered to be having a FALSE value; those that don’t are negated have a TRUE value.

If you want to prove that a formula is a tautology, simply left blank the Premises text editor and write only the conclusion. If you only write a set of premises, but do not provide any conclusion, the Tableaux check whether the set of premises is satisfiable (that is, certain truth values can be assigned to the propositions to make true all the premises) and, if that is the case, shows those sets of values, which are the models of the set of formulas.

The program will also show a schema of the steps followed to solve the Tableaux. For example, given the following set of premises:

A -> (C & A) B -> !(C & A) C -> A

And the conclusion:

!B

The application displays the following message with a counterexample (since the conclusion does not follow from the premises):

A counterexample provided by the Tableaux

And it will show the Tableaux schema that has been built to achieve this result:

Each one of the formulas is numbered on the right side, and, enclosed in brackets, which of them has been used to apply the rule to extend or divide the branches. The closed branches end with a # character.

There is not a single way to build the Tableaux, because normally there are several formulas that are valid candidates for applying the rules, but the final conclusion is always the same. In the case of this implementation, it has applied the following heuristics to select candidate formulas: a conjunctive formula is preferably selected to avoid making too many branches, and it always tries to select a formula that closes a branch when the rule is applied.

Brief explanation of the source code of the Tableaux program

To not extend too much this article, this time I'll make only a brief explanation of the main classes in the source code of the Tableaux project.

There are two classes that implement the elements of the Tableaux, TableauxElementAlpha, which manages the branches that are formed by adding formulas when the rule for conjunctive formulas is applied, and TableauxElementBeta, which manages the ramifications that are formed by applying the rule to the disjunctive formulas. Both inherit from the abstract base class TableauxElementBase.

The TableauxElementAlpha class stores the formulas in a list of KeyValuePair objects, whose key is the index of the formula that has been applied to extract the sub formula, or -1 if it is one of the formulas in the initial set. The _branch variable also contains a KeyValuePair object, which contains a TableauxElementBeta object, along with the index of the formula from which it has been constructed, when the branch is divided into two sub branches.

The TableauxElementBeta class contains two TableauxElementAlpha sub branches, stored in the _fleft and _fright variables.

The properties and common methods are defined in the abstract base class TableauxElementBase, and are as follows:

Closed: This property indicates whether the sub-branch is closed.
Models: It is a method that returns a list of text strings with the values of the variables that constitute a counterexample or a model of the set of input premises.
Contains: This function checks in the sub-branch if exists the formula that is passed as a parameter. It can be used to check whether a particular rule can be applied on the sub-branch, or to check whether the sub-branch is closed or will close, passing the negated formula in the parameter.
PerformStep: This is the highest level method; that is called to execute the next step in the Tableaux. It will return true if it was possible to perform a step, or false otherwise.
WhatIf: With this method we check what would happen in the Tableaux in the case of applying a certain rule in the current branch. It returns a member of the StepResult enumeration, that can be NotAllowed, to indicate that it is not possible to perform the operation, BranchClosed, to indicate that the branch will close, or None, to indicate that nothing relevant will happen.