命题公式合法性的自动判定

摘要：本文就命题公式合法性的自动判定方法进行阐述，首先给出命题的合式公式的相关概念，其次探讨用计算机自动判定命题公式合法性的方法，并对设计过程加以描述。

Abstract： This paper focuses on the methods to judge the legitimacy of a professional formula automatically. Firstly， the relevant concepts over well-formed formula of a proposition are listed. After that， the methods to judge the legitimacy of a propositional formula automatically by a computer are discussed， and the related design process is described at the end.

关键词：命题公式；合法性；自动判定

Key words： professional formula；legitimacy；automatic judgment

中图分类号：TP301 文献标识码：A 文章编号：1006-4311（2015）31-0201-03

0 引言

离散数学是研究离散量的结构及其相互关系的数学学科，是现代数学的一个重要分支。离散数学所研究的思想和方法，广泛地体现在计算机科学技术及相关专业的诸领域，从科学计算到信息处理，从理论计算机科学到计算机应用技术，从计算机软件到计算机硬件，从人工智能到认知系统，无不与离散数学密切相关。

数理逻辑是离散数学一个重要组成部分，又称符号逻辑、理论逻辑，是用数学方法研究推理的形式结构和推理的规律的数学学科。数理逻辑的两个最基本的也是最重要的组成部分，就是“命题演算”和“谓词演算”。

命题是具有具体意义的又具有确定真值的陈述句。命题演算是研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。如果我们把命题看作运算的对象，如同代数中的数字、字母或代数式，而把逻辑连接词看作运算符号，就像代数中的“加、减、乘、除”那样，那么由简单命题组成复合命题的过程，就可以当作逻辑运算的过程，也就是命题的演算。为了实现命题演算，就要将命题符号化，引入命题公式的概念，并对命题公式合法性进行判定。本文就命题公式合法性的自动判定进行阐述，首先给出命题的合式公式的相关概念，其次探讨用计算机自动判定命题公式合法性的方法，并对设计过程加以描述。

1 相关概念

命题：能表达判断的陈述句称作命题，命题分为原子命题和复合命题。

原子命题：不能分解为更简单的陈述语句的命题。

复合命题：由联结词、标点符号和原子命题复合构成的命题。

命题标识符：表示命题的符号称为命题标识符。在数理逻辑中，使用大写字母、带下标的大写字母或用方括号括起的数字表示命题。

命题常量：一个命题标识符如表示确定的命题，就称为命题常量。

命题变元：如果命题标识符只表示任意命题的位置标志，就称为命题变元。

命题公式：命题演算的合式公式（wff），规定为：

①单个命题变元（常量）本身是一个合式公式。

②如果A是合式公式，那么A是合式公式。

③如果A和B是合式公式，那么（A∧B），（A∨B），（AB）和（A？圮B）都是合式公式。

④当且仅当能够有限次地应用①、②、③所得到的包含命题变元，联结词和括号的符号串是合式公式。

2 问题描述与分析

从上述命题公式的定义可以看出一个合法的命题公式是由命题变元（常量）、联结词以及括号这样三种符号按照一定的规则所构成的符号串，因此要判断命题公式的合法性首先要将这三种符号区分，下面就针对这三种符号分别展开讨论。

2.1 命题变元（常量）

命题变元（常量）是由命题标识符来表示的，而命题标识符使用大写字母、带下标的大写字母或用方括号括起的数字来表示。

2.1.1 单个命题变元的判定

一个合法的单个命题变元应当由大写字母或左方括号开始。如果由大写字母开始则后面不能出现方括号，但可以有或没有数字下标。当没有数字下标时单个的大写字母就是一个单个命题变元，如命题变元P；当大写字母后面出现数字下标时从大写字母开始到数字下标结束的字符串表示一个命题变元，如命题变元P1、命题变元Q12。如果单个命题变元由左方括号开始，则左方括号后只能跟数字字符串，数字后以右方括号作为一个命题变元的结束，如命题变元[1]、命题变元[12]等。

2.1.2 命题公式中命题变元之间的合法性判定

在一个合法的命题公式中，不同的命题变元不能连续出现，如PQ、A[1]都不是合法的命题公式，命题变元与命题变元之间必须由联结词连接，如A∧B，A∨B，AB和A？圮B都是合法的命题公式。

2.2 括号

在命题公式中由于联结词存在不同的优先级，为了让命题公式中的某个子公式具有高的优先级可以使用括号。首先括号必须成对使用，多个括号可以嵌套使用，应先有左括号再有右括号，有多少个左括号‘（’就应当有多少个右括号‘）’与之相匹配；其次在合法的命题公式中左右括号不能连续出现，如（）A不是合法的命题公式。第三，左括号不能出现在二元联结词的前方，右括号不能出现在二元联结词的后方，如A（∧B）、（A∧）B都不是合法命题公式。

2.3 联结词

命题公式中常用的联结词一共有九个，分别是：、∧、∨、、？圮、、、、。这九个联结词中是一元联结词，其余8个都是二元联结词。

2.3.1 一元联结词合法性判定

是一元联结词，在命题公式中只能出现在单个命题变元或命题子公式的前方，不能出现在单个命题变元或命题子公式的后方，如A是合法命题公式而A不是合法命题公式。多个联结词可连续出现，比如A是合法命题公式，表示A的否定。

2.3.2 二元联结词合法性判定

二元联结词在命题公式中用于联结两个命题变元或命题子公式，来表达命题变元或命题子公式之间的逻辑关系。因此两个或两个以上二元联结词在一个合法的命题公式中不能连续出现，一个二元联结词的前方和后方应各有一个命题子公式。命题子公式可以是单个命题变元也可以是命题的合式公式，如A∧B、A（B∨C）、A？圮B都是合法命题公式而A∧∨B不是合法命题公式。要特别提出的是二元联结词与一元联结词可以连续出现，但如果出现必须出现在其他二元联结词的后方而不能出现在其他二元联结词的前方，比如A？圮B是合法命题公式而A？圮B不是合法命题公式。只是因为A和B都是合法命题子公式，通过联结词？圮联结所以A？圮B是合法命题公式；而A不是合法命题公式所以A？圮B也不是合法命题公式。

3 系统实现

3.1 模块图设计

为了实现命题公式合法性的自动判定，针对上面所提出的在命题公式合法性的判断中应注意的规则设计以下模块，如图1所示。

其中公式录入与转换模块用于录入待判定的命题公式，为了降低判断的难度，提高判断的效率按照一定的公式转换规则对待判断的公式进行转换；括号匹配检测、空括号检测这两个模块用于判定待检测命题公式中括号使用的合法性；命题变元合法性检测、命题变元连续出现检测、命题变元在左括号之前的检测、命题变元在右括号之后的检测这四个模块用于判定待检测命题公式中命题变元使用的合法性；左括号在二元联结词前的检测、右括号在二元联结词后的检测、二元联结词连续出现检测、联结词在右括号或二元联结词前的检测、联结词在命题变元之后的检测这五个模块用于判定待检测命题公式中联结词使用的合法性。在图1所示的功能模块中除录入与转换模块外其余模块将非法命题公式可能出现的问题都罗列出来，在对待判定公式进行检测时对以上所有令命题公式非法的条件均进行检测，如果所有检测均能通过，那么该命题公式就为一个合法命题公式，如果待判定公式在以上任意一种检测中被报为不是合法命题，那么该命题公式就不是一个合法命题公式。

3.2 算法描述

由于该公式的定义是由递归的形式给出的，那么我们依然可以应用递归思想去对公式进行判断。下面就其中几个模块的实现加以阐述：

3.2.1 公式录入与转换

将待判断的公式录入为字符串变量。为方便系统识别，降低识别难度，提高识别效率，录入后对公式按照不同的字符类别进行转换，定义以下规则：

①所有命题变元使用字符“#”代替；

②二元联结词均使用字符“@”代替；

③联结词均使用字符“！”代替。

例如录入命题公式为：A（B∨C），按照以上的转换规则，待检测命题公式被转换为：

！#@（#@#）。

3.2.2 括号匹配检测

检测括号本身是否匹配：

在一个字符串中括号必须是成对按一定规律出现，否则不是命题公式，具体算法如下：

n=0；

while（*ch！='＼0'）

{if（*ch=='（'）{n++； }

if（*ch=='）'）

{ n--；

if（n

}

ch++； }

if（n！=0） { printf（"该字符串不是合法命题"）；exit（0）； }

例如待测命题公式为A（B∨C），在括号匹配检测前被转换为：！#@（#@#），按照括号匹配检测算法变量n初值为0，当检测到左括号‘（’时执行n+1操作，变量n的值为1，继续向下检测，当检测到右括号‘）’时执行n-1操作，变量n的值为0。整个字符串扫描一遍当变量n的值为0时，说明待测命题公式括号是成对按一定规律出现的，如果变量n的值不为0，那么括号一定不匹配。

3.2.3 空括号检测

检测括号是否本身单独成对出现：

在一个字符串中如果括号本身单独出现而括号中没有任何东西则必不是命题公式，具体算法如下：

while（*ch！='＼0'）

{if（*ch=='（'&&*（ch++）=='）'）

{ printf（"该字符串不是合法命题"）；

exit（0）；

} ch++； }

}

例如待测公式为A∧（ ）B，被转换为：#@（）#，按照空括号检测算法当ch指针指向左括号‘（’时ch++指向右括号‘）’，即左括号‘（’的下一个字符是右括号‘）’，此时括号本身单独成对出现，待测公式不是合法命题公式。

3.2.4 命题变元连续出现检测

命题变元不能连续出现，如PQ就不是合法的命题公式，具体检测算法如下：

while（*ch！='＼0'）

{ ch2=ch+1；

if（*ch=='#'&&*ch2=='#'）

{ printf（"该字符串不是合法命题"）；

exit（0）；

}

ch++；

}

例如待测公式为A（BC），被转换为：！#@（##），按照该检测算法当ch指针指向命题变元B时由于此时命题变元B被转换成为#，此时ch指针指向变量的值为#，而ch2指针指向ch指针所指的下一个字符即命题变元C，由于此时命题变元C也被转换成为#，所以ch2指针所指变量的值也为#，即命题变元连续出现，待测公式不是合法命题公式。

其它模块算法与此模块算法实现类似，在此就不一一赘述了。

3.2.5 判定实例

例如待测公式为（Q∧P）∨R，判定结果如图2所示。

例如待测公式为（Q∧P）∨R∧，判定结果如图3所示。

4 结束语

本文给出了用计算机对任意命题公式合法性自动判定的算法。针对命题公式中命题变元表示方法多样、联结词种类多的特点设定公式转换规则对待判断的公式进行转换，降低判定难度。详细分析各种导致命题公式非法的原因，针对这些原因编写了十一个检测命题公式非法的功能模块。一个待判定公式如果能够通过所有检测模块的检测，那么该公式就是一个合法命题公式。

命题公式合法性的判别是命题逻辑的基础，因此本文给出的算法为利用计算机解决命题逻辑中的其它问题奠定了基础。

参考文献：

[1]左孝凌，刘永才，等著.离散数学[M].上海科学技术文献出版社，2009年7月.

[2]李涛著.数理逻辑引论[M].哈尔滨工业大学出版社，2011年11月.

[3]张会凌.命题公式真值表的生成与公式类型的机械判定[J].甘肃联合大学学报（自然科学版），2006，20（01）：25-27.