命题公式主析范式的自动生成系统

 1 选题背景
逻辑学是研究思维和论证的科学，也就是研究关于人类推理的学问。在20世纪的下半个世纪，伴随着计算机科学技术的迅猛发展，新的逻辑学分支——数理逻辑也发展起来。数理逻辑也称为符号逻辑，是一门运用数学的方法来研究推理的形式结构和推理规律的边缘性学科。其内容相当广泛，包括逻辑演算（命题演算与谓词演算）、公理集合论、证明论、递归函数论等，其中逻辑演算是其它各部分的基础。它在逻辑电路、自动控制、人工智能、程序设计、数据库理论以及计算机科学的其它领域有着广泛的应用。人工智能是研究使计算机来模拟人的某些思维过程和智能行为，主要包括计算机实现智能的原理、制造类似于人脑智能的计算机，使计算机能实现更高层次的应用。人工智能涉及的计算机科学、心理学、哲学和语言学等学科。但最主要的依然是计算机科学的范畴，人工智能对于逻辑的计算十分依赖，尤其是进行推理的时候，在这方面对命题逻辑的研究就有着十分重要的贡献，它是人工智能所能发挥的作用有多大，所能覆盖的范畴有多广的决定性因素之一，所以求一个给定的命题公式的主析取范式或主合取范式是命题逻辑中一类很重要的工作，它是命题分解和进一步进行机器处理的基础。通过这个系统，用户可以更加方便的得出命题公式主范式，有助于对命题逻辑的学习和研究。
2 研究内容
本文主要介绍了命题公式主范式的自动生成方法。首先，给出了主范式的基础定义及相关定理，并对其中定义给出解释，定理做出解释；探讨出主范式的求法——真值表求法，并对设计过程加以描述，包括了命题公式识别，命题公式转译以及命题公式真值表生成三个部分，可以实现命题公式的合法性判断，大小项的生成，命题公式的真值以及命题公式主范式的生成。
3 概念描述
3.1 大项与小项 小项：n个命题变元的合取式，称作布尔合取或小项，其中每个变元与它的否定不能同时存在，但两者必须出现且仅出现一次。
大项：n个命题变元的析取式，称作布尔析取或小项，其中每个变元与它的否定不能同时存在，但两者必须出现且仅出现一次。
3.2 主析取范式及主合取范式 主析取范式：对于给定的命题公式，如果有一个等价公式仅由小项的析取所组成，则该等价式称作原式的主析取范式。
主合取范式：对于给定的命题公式，如果有一个等价公式仅由大项的合取所组成，则该等价式称作原式的主合取范式。
3.3 主析取范式及主合取范式的求取方法 主析取范式及主合取范式的求取方法有真值表法、等价变换法等，本系统采用真值表法求取主析取范式及主合取范式，故只对这种方法加以描述，其他方法在这里概不描述。
在真值表中，一个公式的真值为T的指派所对应的小项的析取，即为此公式的主析取范式。
在真值表中，一个公式的真值为F的指派所对应的大项的合取，即为此公式的主合取范式。
4 模块设计
由于无法保证用户输入一定准确无误，而主范式求取的算法默认所得到的命题公式是正确的，所以一旦命题公式输入出错，则有可能输出错误的结果，甚至引起本系统的崩溃，所以为了确保程序能正常进行，在进行主范式生成运算前必须验证命题公式是否正确。
由于计算机的计算速度和存取速度十分快速，而真值表法求取主析取范式及主合取范式实现起来比较简单，所以选用了真值表法。这就需要模拟出一个可以填入和修改真值的真值表，最终利用真值表得出命题公式大小项进而得出主范式。
因此主范式生成包括公式识别、真值表生成以及主范式生成三大模块。其中公式识别分为公式格式化、公式转译、公式化简并判断。真值表生成分为真值表初始化，真值表填入。模块图如图1所示。
5 系统实现
首先给出主范式生成的流程图。如图2所示。
5.1 命题公式的识别 命题公式识别算法采用递归思想对字符串进行重复简化直到变成一个命题变元，如果不能则判断该字符串不是命题公式。
我们知道，命题公式需要遵循四个规定：
（1）单个命题变元是一个合式公式；
（2）如果A是合式公式，则□A是合式公式；
（3）如果A和B是合式公式，那么（A∧B），（A∨B），（A→B）和（A□B）都是合式公式；
（4）当且仅当能够有限次地应用（1），（2），（3）所得到的包含命题变元，连接词和括号的符号串是合式公式。
由于该公式的定义是由递归的形式给出的，那么我们依然可以应用递归思想去对公式进行判断。
为方便系统识别，我们首先定义以下标准：
1）所有的字母使用字符“*”代替；
2）除 “□”符与括号之外的所有符号均使用“@”代替。
当传入字符串之后，首先去掉空括号与连续的两个“□”符，之后运用上述标准做字符替换。由于我们的工作是判断该字符串是否是一个合法的命题公式，在判断的最后只需要返回一个true值或者false值。也就是说A与（A∧B）的返回值是一样的。
在这里我们编写了一个剪掉算法，该算法可以剪掉字符串中的任意字符或者代替字符串中的任意字符。
这样的话，我们就可以将A∧B，□A，（A）全部替换为A，使用循环直到字符串的长度不再发生变化时循环结束，判断其是否为一个单一命题变元。若是则返回TRUE值；若不是则返回FALSE值。
5.2 真值表生成 当我们人为的在纸上构造真值表时，只需要先列出原始命题变元及拆分出的命题公式，通过自己的计算依次填入真值即可，问题是如何在计算机上实现这一系列过程真值表前N列是N个原始的命题变元，我们为了得到整个公式的，需要一点点将其化简，即将类似“□P”，“PVQ”，“（P）”之类的命题公式化简成为“P”，同时应用公式中的符号和命题变元，首先识别符号让计算机知道这个公式是做合取，析取，取反，条件还是双条件，再根据公式中的命题变元计算出该公式对应的真值存入真值表，记录为一个新的命题变元而非公式，如此反复，直到最终整个原始公式只剩下一个命题变元，这个命题变元即为所求公式的真值。
本系统为了节省硬盘空间，以及提高效率，直接使用了arraylist数组代替在数据库中建表实现真值表的生成，我将arraylist定义成boolean型数组类型，这样每个arraylist中的一个元素其实都是真值表中的一列，而且可以任意添加，有效控制数量和空间复杂程度，这个类就是对真值表的初始化，运行后的结果就如同画好了真值表表格并已填入初始的单一命题变元的初始真值，为随后的主范式计算做准备。
5.3 大小项的生成 在计算出了真值之后，利用真值即可得出大项与小项，只要提取出前面定义的arraylist的最后一组，那一组里存的正是命题公式的真值，在得出大小项后可以生主范式。在web上只需要写上一个调用getString（）方法的语句即可打印出来。
这里的原理类似于公式识别，也是将命题公式想办法化简，不同的是，每化简一次都要修改真值表，也就是说在原先的arraylist数组后面再加一个元素，如此一来最后得到的元素必定存储着命题公式的真值，大小项随即得出。
5.4 主范式生成 在有了大小项之后，根据真值表法即可得出主合取范式以及主析取范式，由于在计算过程中，使用的符号都是计算机中的符号而非离散数学专业符号，但是给用户的答案必须是专业的，所以在生成主范式的同时，也要对符号进行标准化转化。