使用图表进行逻辑计算

• 下载 PLTableaux 解决方案的源代码 - 241.2 KB

引言

语义表演算是一种逻辑计算工具，可以作为构建自动定理证明器的基础。

表演算逻辑在 PLTableauxCalculator 类库中实现。PLTableaux 应用程序展示了如何使用该库。该解决方案使用 C# 和 Visual Studio 2015 编写。

在此版本的 tableaux 中，我将其应用于命题逻辑，也称为零阶逻辑。尽管这种逻辑系统表达能力有限，但它是可判定的，这意味着你总是可以找到一种算法来判断一个公式是否是重言式，或者它是否是从一系列前提得出的结论。

tableaux 方法可以应用于多种逻辑。例如，一阶逻辑是一种更强大、表达力更强的逻辑系统，但其表达能力的提升是以牺牲可判定性为代价的。没有一个通用的算法可以总是判断一个结论是否源自一组前提。无论如何，如果你对将此算法应用于一阶逻辑感兴趣，可以访问我的博客（此处为西班牙语）。

背景

命题逻辑的主要组成部分当然是命题。命题是一个可以是真或假的陈述，例如，所有人都终有一死。

使用命题，您可以使用以下运算符或连接词构建公式：

• 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)

将它们写在应用程序中相应的文本框中。! 键表示否定，& 表示与运算符，| 表示或运算符，< 表示蕴含，> 表示双蕴含。文本框会将它们转换为更标准的符号。

在编写公式时，您必须考虑运算符的优先级，即 非，然后是 蕴含，然后是 与 / 或。p → q ˄ r 与 p → (q ˄ r) 不同。

然后，您只需点击处理按钮

计算结果显示在右侧的文本框中，结论下方显示表演算。让我们看看构建它的算法是什么。

您可以做的第一件事，虽然不是强制性的，是将所有公式转换，使它们只包含 非、与 和 或 运算符。这可以通过我之前提到的转换规则来完成。这使得过程更容易。

然后，所有被否定的公式都必须使用以下规则进行处理：

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

表演算是反驳程序，因此，它会试图反驳结论的否定源自前提。因此，下一步是否定结论。您可以使用否定规则来做到这一点。

表演算是公式树。您从创建根分支开始，其中包含前提和被否定的结论。

然后，一个迭代过程开始，遵循以下规则：

您可以在一个开放分支的末尾添加新公式，前提是该公式尚未出现在该分支中，从最终位置到树的根部。

在开放分支的末尾，您可以添加一个公式的简化版本（¬¬ϕ = ϕ）。

形如 ϕ ˄ ψ 的公式可以分解为两个公式 ϕ 和 ψ，它们可以添加到出现该公式的开放分支的末尾。这称为 alpha 规则。

形如 ϕ ˅ ψ 的公式可以分解为两个公式 ϕ 和 ψ，将树分支成两个新分支，每个分支都以其中一个新公式开头。这称为 beta 规则。

当一个分支中出现一个公式及其否定时，该分支将被关闭，不能再扩展。这由 # 字符表示。

当所有分支都关闭，或者您无法再进行任何公式分解时，表演算终止。在第一种情况下，您已证明结论源自前提。在第二种情况下，结论不源自前提，您可以从开放分支中获取反例，获取分支中所有单个命题。如果命题出现为 p，则添加 p=True 作为反例的一个组成部分；如果出现 ¬p，则添加 p=False。

这是一个简单的例子。论证是这样的：

如果厨师胜任且食材未过期，那么他准备的蛋糕将是美味的。

厨师胜任。

那么，如果蛋糕不好吃，那是因为食材过期了。

命题是：

• p：厨师胜任
• q：食材过期
• r：蛋糕美味

论证和相应的表演算如下：

位置 1 和 2 的公式是前提，位置 3 的是已否定的结论。第一个操作是对位置 3 的公式应用 alpha 规则，这在新增的两个公式的右侧标明为 [R 3]。

然后，对公式 1 应用 beta 规则，将树分成两个新分支。右分支关闭，因为公式 r 及其否定都在该分支中。

在左分支中，我们再次应用 beta 规则，并且表演算的所有分支都关闭了。

尝试以下前提：

• p → q
• q ˅ r

以及结论

• (r ˅ ¬p) → q

看看当结论不从前提中得出时会发生什么。您也可以通过只提供一个结论并留空前提来测试一个公式是否是重言式（即，它总是真的，例如 q ˅ ¬q）。另一方面，如果您留空结论并给出一些前提，算法会提供模型（如果存在），这些模型可以同时满足所有公式（即，使它们都为真）。

Using the Code

PLTableauxCalculator 类库有两个不同的命名空间。PLTableauxCalculator.Formulas 包含所有用于处理逻辑表达式的类，而 PLTableauxCalculator.Tableaux 包含实现表演算的类。

用于实现公式的两个类是 Formula 和 Predicate，它们都是 abstract 类 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' });
    }
}

由于谓词在所有公式中必须是唯一的，因此有一个静态列表来获取它们的规范形式。

该类实现了 IEquatable 和 IComparable，以简化在树中查找公式或其否定，以及在 _predicates 列表中查找谓词。

一个 Formula 由一个或两个参数和一个运算符组成，当有两个参数时，运算符是必需的，而只有一个参数时，运算符是可选的。

参数也可以是公式，或者是 Predicate 类的谓词。您可以使用从 a 到 z 的任何字母组合来定义谓词。

因此，Operator 属性显然返回 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 属性测试树的某个分支是否关闭。根分支中此属性的值可用于测试整个表演算是否关闭。

要测试一个分支是否包含某个公式，有两个方法：Contains 和 Negate。要判断一个分支是否关闭，必须检查是否存在该公式的否定。

WhatIf 方法用于测试多种可能的操作并选择最佳选项。通常，最佳选项是优先选择关闭一个分支的操作，并且使用 alpha 规则优于 beta 规则。此方法还会检查是否允许执行特定操作。

一旦决定执行何种操作，就必须使用 ExecuteStep 方法来执行它。PerformStep 方法是一个高级方法，它使用 WhatIf 选择操作，并使用 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 类中，当您按下处理按钮时，此类的使用方式如下：

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);
    }
}

就这样！享受这个逻辑工具，用它来处理您自己的论证。感谢阅读！！！

历史

• 2017年1月29日：初始版本