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 a universal algorithm that can decide always 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 one of the three lies, then one of the others will lie too.
You can be sure too that one of the three is a liar.
The conclusion is that, in the best case, only one of the three is truthful.
You can formalice this as follows:
p: first politician liesq: second politician liesr: 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 end 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 appears 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 demonstrated 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 have 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 because the ingredients have expired.
The propositions are:
p: the cook is competentq: the ingredients have expiredr: the cake is delicious
And the argumentation and the corresponding tableaux is like this:
The formulas in 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:
and the conclusion:
To see what happens with a conclusion that doesn't follow from the premises. You too can test if a formula is a tautology (i.e., it is always 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 having 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 if the 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 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 checks if a certain 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 WhatIf, 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, when 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!!!
History
- 29th January, 2017: Initial version
