如何使用tableaux进行逻辑计算
Logical calculation with tableaux
原文作者：Miguel Diaz Kusztrich
原文地址：https://www.codeproject.com/Articles/1167869/Logical-calculation-with-tableaux
译者微博：@从流域到海域
译者博客：blog.csdn.net/solo95
如何使用tableaux进行逻辑计算
- 下载PLTableaux解决方案的源代码 - 241.2 KB
介绍
Semantic tableaux是一个逻辑计算工具，可以作为构建自动理论演示器(automatic theorema demonstrators)的基础。
The tableaux logic(可译为tableaux逻辑)在PLTableauxCalculator类库中实现。PLTableaux应用程序显示如何使用该库。解决方案是在Visual Studio 2015中用C＃编写的。
在这个版本的tableaux中，我已经将它应用于命题逻辑(propositional logic)，也称为零阶逻辑。虽然这个逻辑系统表达性有限，它是可以决定的，这意味着你可以找到一个算法来判断一个公式是重言式(永真式)还是从一系列前提中得到的结论。
该tableaux方法可以应用于大范围的逻辑(logics)中。例如，一阶逻辑就是一个更强大和更有表现力的逻辑系统，但是他们在表达能力方面的收获是以失去可判定性为代价的。没有一个通用的算法能够一直判定(decide)一个结论是否是从一组前提中得出的。不过怎么说，如果你对这个算法在一阶逻辑上的应用感兴趣，你可以访问我的博客(这里是西班牙语版的)。
背景
命题逻辑的主要部分当然是命题。一个命题可以是一个真或假的陈述，例如，所有的人都是凡人。
通过命题，您可以使用以下运算符或连接符来构建公式：
- And(与)(˄)：如果p和q都为真，则p˄q为真。
- Or(或)(˅)：如果p为真或q为真或者两者，p˅q结果为真。
- Negation(非)(¬)：应用于值为真的语句时，结果是假，也可以反过来。
- Implication(蕴含)(→)：p→q表示如果p为真，则q也必须为真。如果p是假的，不管q的真值是多少，公式总是成立的(任何结论都来自一个错误的前提)。它也可以表示为¬p˅q。
- Double implication(双向蕴含，即等价)(↔)：p↔q表示一次(推导中)p→q和q→p同时成立。它也可以表示为(¬p˅q)˄(¬q˅p)。
假设你有一套逻辑公式(这是前提)，你想证明另一个公式是(该)逻辑公式的结论。这被称之为推理：
有三位政要将在电视上发表演讲。我们可以肯定的是，如果这三个人中的一个人撒谎，那么其他两个人之一也会撒谎。
你也可以确定三人中某人是骗子。
结论是，在最好的情况下，三者中只有一个是真的。
你可以这样来形容这个：
p：第一个政客撒谎。
q：第二个政客撒谎。
r：第三个政治撒谎。
那么，前提是：
p→(q˅r)
q→(p˅r)
r→(p˅q)
p˅q˅r
得出的结论是：
(p˄q) ˅ (p˄r) ˅ (q˄r)
(r如果要)把它们写在应用程序中，在相应的文本框中。那!键是非(运算符)(指键盘上的键，后同，译者注)，＆为与运算符，| 是或运算符，<用于蕴含，>用于等价。文本框(自动)将其转换为更加标准的符号。
当您编写公式时，您必须考虑到运算符的优先级，即首先是not(非)，然后是蕴含，再然后是and(与) / or(或)。p→q^r和p→(q^r)是不一样。
然后，您只需点击Process按钮：
演算的结果显示在右边的文本框中，结论的下方显示了图表。我们来看看构建它的算法是什么。
你可以做的第一件事情，虽然不是强制性的，是对所有的公式进行转换，使他们只拥有not，and和or运算符。(转换)可以使用我之前提到的转换规则来完成。转换规则的存在使得转换过程更加容易一点。
接着，所有的否定公式必须使用以下规则进行处理：
- ¬(ϕ ˄ ψ) = ¬ϕ ˅ ¬ψ
- ¬(ϕ ˅ ψ) = ¬ϕ ˄ ¬ψ
- ¬¬ϕ = ϕ
这是一个反驳(refutation)的过程，因此，它将试图驳斥结论的否定(驳斥结论的否定即证明结论的肯定，译者注)。因此，下一步就是否定结论。你可以使用否定规则来做到这一点。
tableaux是一个公式树。你可以用前提(premises)和否定结论(negated conclusion)创建根的分支。
然后，按照以下规则开始迭代过程：
从最终位置到树的根，您都可以在开放分支的末尾添加新的公式，前提是该公式不是已经在分支中出现的公式。
在开放分支的末尾，可以添加公式的简化版本(¬¬φ=φ)。
一个ϕ˄ψ形式的公式可以分为两个公式φ和ψ，它们可以被添加到它出现的开放分支的末端。这被称为alpha规则。
ϕ˅ψ 的形式可以分为φ和φ两个公式，将树分成两个新分支，每个分支都从一个新公式开始。这被命名为beta规则。
当一个分支出现一个公式和它的否定时，该分支就关闭了，不能再扩展了。这会被用＃字符标注。
当所有分支关闭，或者不能进行对任何公式进行分解时，tableaux就会被终止。在第一种情况下，你已经(成功)证明结论是从这个前提出发的。在第二种情况下，结论不是从前提出来的，你可以从开放的分支中得到反例，(只需)把分支中的所有单个命题都拿走(这些命题构成反例，译者注)。如果命题显示为p，则将p=True作为反例的一个组成部分，如果出现¬p，则添加p=False(作为反例的一个组成部分)。
这是一个简单的例子。论证(是一个由推导式构成的过程，译者注)是这样的：
如果厨师能胜任，而且配料没有过期，那么他准备的蛋糕将是美味的。
厨师是胜任的。
那么，如果蛋糕不好吃，那是因为食材已经过期了。
命题是：
p：厨师是胜任的。
q：配料已过期。
r：蛋糕很好吃。
论证和相应的tableaux是这样的：
位置1和位置2的公式是前提，位置3的公式是结论的否定。第一个操作是将alpha规则应用到第3个位置上的公式上，两个新公式右侧指示的R 3已经揭示了这个过程。
(即用R 3来表示将alpha规则应用到第3个位置的公式上)
然后，在公式1上应用beta规则，将树分支为两个新的分支。右分支关闭，因为公式r和它们的否定都在分支中。
在左侧分支中，我们再次应用一个beta规则，并关闭了tableaux的所有分支。
用这些前提进行尝试：
p→q
(r˅¬p)→q
并使用这个结论：
(r←p)→q
看看(如果使用)不是从前提出发得到的结论会发生什么结果。你也可以检验一个公式是否是一个重言式(即它总是真的，就像q˅¬q)只能提供一个结论，并将前提留空(即不提供前提)。另一方面，如果把结论留空，并给予一些前提，该算法将提供模型，如果有的话，可以一次满足所有的公式(把他们全部变为真)。
使用代码
PLTableauxCalculator类库有两个不同的名称空间。PLTableauxCalculator.Formulas包含所有被定义来处理逻辑表达式的类，而PLTableauxCalculator.Tableaux包含实现tableaux的类。
用于实现公式的两个类是Formula和Predicate，都是抽象类FormulaBase的后代，定义如下：
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' });
}
}由于断言(predicate)在所有公式中必须是唯一的，所以有一个静态的列表来获得一个规范的形式。
该类实现了IEquatable和IComparable，以简化搜索树中的公式或其否定的操作，并在_predicates列表中查找断言(Predicate)。
一个公式是由一个或两个参数和一个运算符组成的，当有两个参数时是必需的，如果只有一个，则是可选的。
参数可以是断言(Predicate)类的公式也可以是断言(Predicate)。您可以使用从a到z的任意字母组合来定义断言(Predicate)。
所以，运算符属性显然返回了FormulaBase对象的运算符。如果没有(返回)运算符，则返回LogicOperator.None。该公式只与not，and和or运算符一起工作。
Negate是一种用于将对象转换为其自身的否定版本的方法。
Operand返回第n个操作数。
所述的 Clone方法返回一个公式的副本。该 Predicate对象不能被复制，因为只有他们中的一个实例存在，所以他们依然在重复的公式中的保持一致。
最后，Parse方法用于在构建过程中解析公式的文本。
关于tableaux类，有两个类，一个用于alpha规则(TableauxElementAlpha)，一个简单的公式列表，另一个来自beta规则(TableauxElementBeta)，由两个alpha规则组成，它们代表tableaux中的分叉树。
两者都是抽象类TableauxElementBase的的后代(子类)，定义如下：
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;
}
}所述_parent变量用于构建公式树。您可以使用Closed属性测试树的分支是否关闭。这个属性在根分支中的值可以用来测试整个tableaux是否是关闭(状态)。
要测试分支是否包含公式，有两种方法：包含和否定。要决定一个分支是否关闭，必须检查是否存在一个公式的否定。
该WhatIf方法用于测试几个可能的操作并选出更好的选择。通常，最好的选择是优先考虑关闭一个分支的操作，并且最好使用一个alpha规则而不是beta规则。这个方法也会检查某些操作是否是允许的。
一旦决定执行什么操作，就必须使用ExecuteStep方法来执行它。该PerformStep方法是同时使用WathIf的高级方法，来选择操作，并且(调用)ExecuteStep执行它。
CalcRect和Draw方法被用于在Graphics对象中绘制tableaux。
但您必须直接处理的类是TableauxCalculator。这是它们的定义：
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;
}
}您可以使用Formula对象列表构建一个TableauxCalculator对象。然后，只需调用Calculate方法来构建tableaux，并且可以使用Models属性来枚举不同的模型(对于一组前提)或反例(对于完整的论证)。使用DrawTableaux方法在Bitmap对象中给出tableaux的表示形式。
例如，这是如何在plTableauxForm类中使用这个类，然后你需要按下Process按钮：
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);
}
}就是这样。快点用你自己的论证享受这个逻辑工具吧。感谢您的阅读！