[译]使用Tableaux进行逻辑计算
By robot-v1.0
本文链接 https://www.kyfws.com/ai/logical-calculation-with-tableaux-zh/
版权声明 本博客所有文章除特别声明外,均采用 BY-NC-SA 许可协议。转载请注明出处!
- 15 分钟阅读 - 7433 个词 阅读量 0使用Tableaux进行逻辑计算(译文)
原文地址:https://www.codeproject.com/Articles/1167869/Logical-calculation-with-tableaux
原文作者:Miguel Diaz Kusztrich
译文由本站 robot-v1.0 翻译
前言
Demonstrate or refute a conclusion automatically from a series of premises
从一系列前提中自动展示或反驳结论
介绍(Introduction)
语义表是一种逻辑计算工具,可以作为构建自动定理演示器的基础.(Semantic tableaux are a logical calculation tool which can serve as a basis to build automatic theorema demonstrators.)
tableaux逻辑在PLTableauxCalculator类库中实现. PLTableaux应用程序显示了如何使用该库.该解决方案是使用Visual Studio 2015的C#编写的.(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.)
tableaux方法可应用于多种逻辑.例如,一阶逻辑是一个功能更强大且更具表现力的逻辑系统,但其表现力的提高是以丧失可判定性为代价的.如果从一组前提得出结论,则没有通用的算法可以始终决定.无论如何,如果您对将此算法应用于一阶逻辑感兴趣,则可以(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均为真,则p˄q为真.((˄): p˄q is true if both p and q are true.)
- 要么(Or)(˅):如果p为true或q为true或两者皆有,则p˅q为true.((˅): p ˅ q is true if p is true or q is true, or both.)
- 否定(Negation)(¬):当应用于true语句时,结果为false值,反之亦然.((¬): when applied to a true statement, the result is a false value, and vice versa.)
- 意义(Implication)(→):p→q表示,如果p为true,则q也必须为true.如果p为假,无论真值具有q,该公式始终为真(任何结论均来自假前提).也可以表示为.((→): 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表示p→q和q→p一次.它也可以表示为(pp q)˄(˄q p).((↔): 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(p):第一位政客的谎言.(: first politician lies.) q(q):第二个政客的谎言.(: second politician lies.) [R(r):第三位政客的谎言.(: third politicion lies.)
然后,前提是:(Then, the premises are:)
p→(q˅r)(p → (q ˅ r)) q→(p˅r)(q → (p ˅ r)) r→(p˅q)(r → (p ˅ q)) ˅(p ˅ q ˅ r)
结论是:(and the conclusion is:)
(p ˄ q)˅(p ˄ r)˅(q ˄ r)((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,)|(|)对于or运算符,(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(p → q ˄ r)是不一样的(is not the same that)p→(q ˄ r)(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规则(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(p),添加(, add)p =真(p=True)作为反例的一部分(如果出现)(as a component of the counterexample, if it appears)¬p(¬p),添加(, add)p =假(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(p):厨师有能力.(: the cook is competent.) q(q):成分已过期.(: the ingredients have expired.) [R(r):蛋糕很好吃.(: the cake is delicious.)
参数和相应的表格如下所示:(And the argumentation and the corresponding tableaux is like this:)
位置1和2的公式是前提,位置3的公式是否定结论.第一项操作是将alpha规则应用于公式的第3个位置,该位置显示在添加的两个新公式的右侧,(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]([R 3]).(.)
然后,将beta规则应用于公式1,将树分成两个新分支.右分支被关闭,如公式(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(r)和它们的否定都在分支中.(and their negation are both in the branch.)
在左侧分支中,我们再次应用beta规则,并且封闭了场景的所有分支.(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(p → q) ˅(q ˅ r)
和结论:(and the conclusion:)
(r˅p)→q((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(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)
PLTableauxCalculator类库具有两个不同的名称空间.(The PLTableauxCalculator class library has two different namespaces.)PLTableauxCalculator.Formulas(PLTableauxCalculator.Formulas)包含定义用于处理逻辑表达式的所有类,而(contains all the classes defined to process the logic expressions, whereas)PLTableauxCalculator.Tableaux(PLTableauxCalculator.Tableaux)包含实现表格的类.(contains the class that implement the tableaux.)
用于实现公式的两个类是Formula和Predicate,它们都是抽象类FormulaBase的后代,定义如下:(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)quaqua(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)类.您可以使用字母从a到z的任意组合来定义谓词.(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)返回第n个操作数.(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.)
关于tableaux类,有两个类,一个用于alpha规则((Regarding the tableaux classes, there are two classes, one for the alpha rules ()TableauxElementAlpha(TableauxElementAlpha)),一个简单的公式列表以及另一个Beta规则((), a simple list of formulas, and another fro the beta rules ()TableauxElementBeta(TableauxElementBeta)),它由两个alpha规则组成,因为它们代表了桌面树中的分支.(), which is composed with two alpha rules, as they represent bifurcations in the tableaux tree.)
两者都是抽象类的后代(Both are descendant of the abstract class)TableauxElementBase(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)方法用于测试几种可能的操作,然后选择哪种方法更好.通常,最好的选择是优先选择关闭一个分支的操作,最好使用alpha规则而不是beta.此方法还检查是否允许某些操作.(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(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(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(TableauxCalculator)带有列表的对象(object with a list of)式(Formula)对象.然后,只需调用Calculate方法即可建立表格,您可以使用(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(DrawTableaux)在表格中表示画面的方法(method to give a representation of the tableaux in a)位图(Bitmap)目的.(object.)
例如,这就是此类在(This is, for example, how this class is used in the)plTableaux表格(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!!!)
许可
本文以及所有相关的源代码和文件均已获得The Code Project Open License (CPOL)的许可。
C# .NET Dev Architect AI algorithms DLL 新闻 翻译