## Introduction

Semantic tableaux are a logical calculation tool which can serve as a basis to build automatic theorema demonstrators.

The tableaux logic is implemented in the PLTableauxCalculator class library. The PLTableaux application shows how to use that library. The solution is written in C# with Visual Studio 2015.

In this version of the tableaux, I have applied it to the propositional logic, also called zeroth order logic. Although this logic system has a limited expressiveness, it is decidable, what means that you can ever find an algorithm to decide if a formula is a tautology or if it is the conclusion from a series of premises.

The tableaux method can be applied to a wide range of logics. The first order logic, for example, is a more powerful and expressive logical system, but their gain in expressiveness is at the cost of losing decidability. There is not an universal algorithm that can decide allways if a conclusion follows from a set of premises. Anyway, if you are interested in the application of this algorithm to first order logic, you can visit my blog (here in spanish).

## Background

The principal component of propositional logic is, of course, the proposition. A proposition is an statement that can be true or false, for example, **all men are mortal**.

With the propositions, you can build formulas using the following operators or connectives:

**And** (˄): p˄q is true if both p and q are true. **Or** (˅): p ˅ q is true if p is true or q is true, or both. **Negation** (¬): when applied to a true statement, the result is a false value, and vice versa. **Implication** (→): p → q means that, if p is true, then q must be true too. If p is false, no matter what truth value has q, the formula is true always (any conclusion follows from a false premise). It can be expressed also as ¬p ˅ q. **Double implication** (↔): p ↔ q means that p → q and q → p at once. It can be expressed too as (¬p ˅ q) ˄ (¬q ˅ p).

Suppose that you have a set of logic formulas (the premises) and you want to demonstrate that another formula is a logic conclusion of them. Say that this is the reasoning:

There are three politicians that are going to give a speech in TV. We can be sure that, if someone of the three lies, then someone of the others will lie too.

You can be sure too that someone of the three is a liar.

The conclusion is that, in the best case, only one of the three is truthfull.

You can formalice this as follows:

**p**: first politician lies.

**q**: second politician lies.

**r**: third politicion lies.

Then, the premises are:

**p → (q ˅ r)**

q → (p ˅ r)

r → (p ˅ q)

p ˅ q ˅ r

and the conclusion is:

**(p ˄ q) ˅ (p ˄ r) ˅ (q ˄ r)**

Write them in the application, in the corresponding text boxes. The **!** key is for the negation, **&** for the and operator, **|** for the or operator, **<** for the implication and **>** for the double implication. The text boxes translate them into a more standard notation.

You have to take into account the precedence of the operators, which is **not**, then **implications**, then **and** / **or**, when you write the formulas. **p → q ˄ r** is not the same that **p → (q ˄ r)**.

Then, you only have to click the Process button:

The result of the calculus is shown in the text box at right, and the tableaux below the conclusion. Let's see what is the algorithm to build it.

The first thing you can do, although is not mandatory, is to convert all the formulas so that they only have the **not**, **and** and **or** operators. This can be accomplished using the conversion rules that I have mentioned previously. This makes the process easier.

Then, all the negated formulas must be processed by using the following rules:

- ¬(ϕ ˄ ψ) = ¬ϕ ˅ ¬ψ
- ¬(ϕ ˅ ψ) = ¬ϕ ˄ ¬ψ
- ¬¬ϕ = ϕ

The tableaux is a procedure of refutation, so, it will try to refute that the negation of the conclusion follows from the premises. The next step, thus, is negate the conclusion. You can use the negation rules to do so.

The tableaux are a formula tree. You start to create the root branch with the premises and the negated conclusion.

Then, an iterative process starts, following these rules:

You can add new formulas at the ennd of an open branch, provided that the formula don't appear already in this branch, from the final position to the root of the tree.

At the end of an open branch, you can add a simplified version of a formula (**¬¬ϕ = ϕ**).

A formula in the form **ϕ ˄ ψ** can be divided in two formulas, **ϕ** and **ψ**, that can be added to the end of the open branch where it appear. This is called an **alpha rule**.

A formula of the form **ϕ ˅ ψ** can be divided in two formulas, **ϕ** and **ψ**, branching the tree in two new branches each one of them starting with one of the new formulas. This is named a **beta rule**.

When in a branch appear a formula and their negation, the branch is closed and it cannot be extended anymore. This is denoted by the **#** character.

When all the branches are closed, or you cannot make any formula decomposition, the tableaux is terminated. In the first case, you have demonstrate that the conclusion follows from the premises. In the second, the conclusion doesn't follow from the premises, and you can get counterexamples from the open branches, taking all the single propositions in the branch. If the proposition appears like **p**, add **p=True** as a component of the counterexample, if it appears **¬p**, add **p=False**.

This is a simple example. The argumentation is like this:

If the cook is competent and the ingredients are not expired, then the cake that he would prepare would be delicious.

The cook is competent.

Then, if the cake is not delicious, it is due to that the ingredients are expired.

The propositions are:

**p**: the cook is competent.

**q**: the ingredients have expired.

**r**: the cake is delicious.

And the argumentation and the corresponding tableaux is like this:

The formulas in the position 1 and 2 are the premises, the one in the position 3 is the negated conclusion. The first operation is to apply the alpha rule to the formula at the 3 position, which is indicated at the right of the two new formulas added, **[R 3]**.

Then, a beta rule is applied to the formula at 1, branching the tree in two new branches. The right branch is closed, as the formula **r** and their negation are both in the branch.

In the left branch, we apply again a beta rule, and all the branches of the tableaux are closed.

Try with these premises:

**p → q**

q ˅ r

and the conclusion:

**(r ˅ ¬p) → q**

To see what happens with a conclusion that doesn't follow from the premises. You can too test if a formula is a tautology (i.e. it is allways true, like **q ˅ ¬q**) providing only a conclusion, and left blank the premises. On the other hand, if you left blank the conclusion and give some premises, the algorithm provides models, if any, that can satisfy all the formulas at once (i.e. make them all true).

## Using the code

The PLTableauxCalculator class library has two different namespaces. **PLTableauxCalculator.Formulas** contains all the classes defined to process the logic expressions, whereas **PLTableauxCalculator.Tableaux** contains the class that implement the tableaux.

The two classes used to implement the formulas are Formula and Predicate, both descendants of the abstract class FormulaBase, defined as follows:

public abstract class FormulaBase : IComparable<FormulaBase>, IEquatable<FormulaBase>
{
protected static List<FormulaBase> _predicates = new List<FormulaBase>();
public FormulaBase()
{
}
public static List<FormulaBase> Predicates
{
get
{
return _predicates;
}
}
public static void Clear()
{
_predicates.Clear();
}
public abstract LogicOperator Operator { get; }
public virtual void Negate() { }
public abstract FormulaBase Operand(int n);
public abstract FormulaBase Clone();
public abstract int CompareTo(FormulaBase other);
public abstract bool Equals(FormulaBase other);
public virtual string Parse(string expr)
{
return expr.TrimStart(new char[] { ' ', '\n', '\r', '\t' });
}
}

As the predicates must be unique along all the formulas, there are a static list of them to get ever a canonical form.

The class implement the **IEquatable** and **IComparable** to simplify the search of a formula or their negation in the tree, and to find predicates in the **_predicates** list.

A **Formula** is composed by one or two arguments and an operator, which is mandatory when there are two arguments and optional in case of have only one.

The arguments can be formulas too, or predicates, of the **Predicate** class. You can use any combination of letters, from a to z, to define a predicate.

So, the **Operator** property returns, obviously, the operator of the **FormulaBase** object. If there is not operator, it will return **LogicOperator.None** as a result. The formulas work only with the **not**, **and** and **or** operators.

**Negate** is a method used to convert the object in a negated version of itself.

**Operand** returns the nth operand.

The **Clone** method returns a copy of the formula. The **Predicate** objects can't be copied, as only one instance of them exists, so they remain the same in the duplicated formula.

Finally, the **Parse** method is used to parse the text of the formula in the building process.

Regarding the tableaux classes, there are two classes, one for the alpha rules (**TableauxElementAlpha**), a simple list of formulas, and another fro the beta rules (**TableauxElementBeta**), which is composed with two alpha rules, as they represent bifurcations in the tableaux tree.

Both are descendant of the abstract class **TableauxElementBase**, defined as follows:

public abstract class TableauxElementBase
{
protected TableauxElementBase _parent;
protected static int _fcnt;
public TableauxElementBase(TableauxElementBase parent, FormulaBase f)
{
_parent = parent;
}
public static void Initialize()
{
_fcnt = 1;
}
public abstract bool Closed { get; }
public abstract List<string> Models(List<string> m);
public abstract bool Contains(FormulaBase f);
public abstract bool PerformStep();
public abstract void ExecuteStep(FormulaBase f, int origin);
public abstract StepResult WhatIf(FormulaBase f);
public abstract void Draw(Graphics gr, Font f, RectangleF rb);
public abstract RectangleF CalcRect(Graphics gr, Font f, RectangleF rb);
protected string RemoveBrackets(string s)
{
if (s.StartsWith("("))
{
s = s.Substring(1);
}
if (s.EndsWith(")"))
{
s = s.Substring(0, s.Length - 1);
}
return s;
}
protected FormulaBase Negate(FormulaBase fn)
{
if (fn is Formula)
{
fn.Negate();
if (fn.Operator == LogicOperator.None)
{
fn = fn.Operand(1);
}
}
else
{
fn = new Formula(fn, null, LogicOperator.Not);
}
return fn;
}
}

The **_parent** variable is used to build the formula tree. You can test if a branch of the tree is closed with the **Closed** property. The value of this property in the root branch can be used to test i fthe entire tableaux is closed.

To test if a branch contains a formula, there are two methods: **Contains** and **Negate**. To decide if a branch is closed, the existence of the negation of a formula must be checked.

The **WhatIf** method is used to test several possible operations and select which that is the better option. Usually the best option is to give preference to operations that close one branch, and is better to use an alpha rule than a beta. This method also check if acertain operation is allowed.

Once decided what operation perform, the method **ExecuteStep** must be used to execute it. The **PerformStep **method is a high level method that uses both **WathIf**, to select the operation, and **ExecuteStep** to perform it.

The **CalcRect** and **Draw** methods are used to draw the tableaux in a **Graphics** object.

But the class with which you have to deal directly is **TableauxCalculator**. This is their definition:

public class TableauxCalculator
{
private TableauxElementAlpha _root;
public TableauxCalculator(List<Formula> premises)
{
TableauxElementBase.Initialize();
_root = new TableauxElementAlpha(null, premises[0]);
for (int ix = 1; ix < premises.Count; ix++)
{
_root.AddFormula(premises[ix]);
}
}
public List<string> Models
{
get
{
List<string> m = new List<string>();
m = Complete(_root.Models(m));
for (int ix = m.Count - 1; ix > 0; ix--)
{
if (Duplicated(m[ix], m, ix))
{
m.RemoveAt(ix);
}
}
return m;
}
}
public bool Calculate()
{
while ((!_root.Closed) && (_root.PerformStep())) ;
return _root.Closed;
}
public Bitmap DrawTableaux()
{
Bitmap bmp = new Bitmap(1, 1);
Graphics gr = Graphics.FromImage(bmp);
Font f = new Font("Courier New", 20f, FontStyle.Regular, GraphicsUnit.Pixel);
RectangleF rect = _root.CalcRect(gr, f, RectangleF.Empty);
bmp = new Bitmap((int)rect.Width, (int)rect.Height);
gr = Graphics.FromImage(bmp);
gr.SmoothingMode = SmoothingMode.AntiAlias;
gr.FillRectangle(Brushes.White, rect);
_root.Draw(gr, f, rect);
f.Dispose();
return bmp;
}
private bool Duplicated(string s, List<string> l, int index)
{
string[] parts = s.Split(';');
for (int ix = index - 1; ix >= 0; ix--)
{
string[] other = l[ix].Split(';');
int c = 0;
foreach (string sp in parts)
{
if (other.Contains<string>(sp))
{
c++;
}
}
if (c == parts.Length)
{
return true;
}
}
return false;
}
private List<string> Complete(List<string> m)
{
for (int ix = 0; ix < m.Count; ix++)
{
string[] parts = m[ix].Split(';');
if (parts.Length < FormulaBase.Predicates.Count)
{
foreach (FormulaBase fp in FormulaBase.Predicates)
{
Regex rex = new Regex(fp.ToString() + "=[TF]");
if (!rex.IsMatch(m[ix]))
{
m[ix] += ";" + fp.ToString() + "=F";
}
}
}
}
return m;
}
}

You can build a **TableauxCalculator** object with a list of **Formula** objects. Then, simply call the Calculate method to build the tableaux and you can use the **Models** property to enumerate the different models (in the case of a group of premises) or counterexamples (in the case of a complete argumentation). Use the **DrawTableaux** method to give a representation of the tableaux in a **Bitmap** object.

This is, for example, how this class is used in the **plTableauxForm** class, qhen you press the **Process** button:

private void bProcess_Click(object sender, EventArgs e)
{
try
{
txtResults.Text = "";
List<Formula> lf = new List<Formula>();
FormulaBase.Clear();
if (!string.IsNullOrEmpty(txtPremises.Text))
{
StringReader sr = new StringReader(txtPremises.Text);
string f = sr.ReadLine();
while (!string.IsNullOrEmpty(f))
{
Formula fp = new Formula();
f = fp.Parse(f.Trim());
lf.Add(fp);
f = sr.ReadLine();
}
}
if (!string.IsNullOrEmpty(txtConclusion.Text))
{
Formula fc = new Formula();
fc.Parse(txtConclusion.Text.Trim());
fc.Negate();
lf.Add(fc);
}
TableauxCalculator tcalc = new TableauxCalculator(lf);
bool bt = tcalc.Calculate();
List<string> m = tcalc.Models;
string msg;
if (string.IsNullOrEmpty(txtConclusion.Text))
{
if (bt)
{
msg = "The system is unsatisfiable";
MessageBox.Show(msg);
}
else
{
msg = "The system is satisfiable\r\nModels:\r\n";
foreach (string s in m)
{
msg += s + "\r\n";
}
txtResults.Text = msg;
}
}
else
{
if (bt)
{
if (lf.Count > 1)
{
msg = "The conclusion follows from the premises";
}
else
{
msg = "The conclusion is a tautology";
}
txtResults.Text = msg;
}
else
{
msg = "The conclusion doesn't follows from the premises\r\nCounterexamples:\r\n";
foreach (string s in m)
{
msg += s + "\r\n";
}
txtResults.Text = msg;
}
}
pbTableaux.Image = tcalc.DrawTableaux();
}
catch (BadSyntaxException bex)
{
MessageBox.Show("Bad Syntax: " + bex.Message);
}
catch (Exception ex)
{
MessageBox.Show(ex.Message);
}
}

And that 's all. Enjoy this logic tool with your own argumentations. And thanks for reading!!!