基于Web的命题逻辑演算证明验证系统的设计与实现

摘要：形式化方法的时代终于来到。规范语言，定理证明，模型检测已开始用于企业的日常运作，数理逻辑是所有的这些技术的基础,而本次课题主要研究是命题逻辑演算。XML（eXtensible Markup Language）作为网络数据交换和信息集成的工具，以其自描述性、跨平台交换性等特点，成为新一代的网络语言。本课题是利用XML技术在互联网上的独特性，使用Web技术，开发一个模拟数理逻辑的程序，可供本地或者网上教学及自学所用。 关键词：数理逻辑，XML，Web技术。 １　研究背景 “逻辑”浅释 　　中文的“逻辑”显然音译自英文的“logic”。logic又来自中古拉丁文的logica，logica又源自希腊文logos（λóγｏｓ）。logos一般翻译为“逻格斯”，接近于中文里的“道”。 中文的“道”和希腊文“logos”都有以下两层意思： （1）各种事物的定义或者各种活动的规则（西方各门学科的名字都以 -logy缀后的习惯） （2）言说，言谈 　　这两层意思也是相互关联的。言谈是为揭示事物的道理，道理也往往通过言谈得以显示。我们可以构造一个有趣的句子“道道道”，意思是“道说是通往道理的道路”。 在言谈和辩论中，渐渐发展出逻辑学这一领域。从地域来分，古代逻辑学可以分为希腊逻辑学（亚里士多德），印度逻辑学（因明学）和中国逻辑学（墨子名学）。 在以往，逻辑学是哲学的一个分支。1800中期后，逻辑学也成为数学的一个分支。近代以来，逻辑学成为计算机科学的重要基础。根据应用的领域，逻辑可以分为哲学逻辑，数理逻辑和计算逻辑。 数理逻辑与计算机科学的关系 　　首先，从计算模型和可计算性的研究来看，可计算函数和可计算谓词（一种能够能行判定其真值的断言或逻辑公式）是等价的，相互之间可以转化。这就是说，计算可以用函数演算来表达，也可以用逻辑系统来表达。作为计算模型可以计算的函数恰好与可计算谓词是等价的，而逻辑系统又能通过自身的无矛盾性保证这样一种计算模型是合理的。由此可见，作为一种数学形式系统，图灵机及其与它等价的计算模型的逻辑基础是坚实的。人工智能领域的一个重要方向就是基于逻辑的人工智能。 　　实际计算机的设计与制造中，使用数字逻辑技术实现计算机的各种运算的理论基础是代数和布尔代数。布尔代数只是在形式演算方面使用了代数的方法，其内容的实质仍然是逻辑。 　　从计算机程序设计语言方面考察，语言的理论基础是形式语言、自动机与形式语义学。而形式语言、自动机和形式语义学所采用的主要研究思想和方法来源于数理逻辑和代数。程序设计语言中的许多机制和方法，如子程序调用中的参数代换、赋值等都出自数理逻辑的方法。此外，在语言的语义研究中，四种语义方法最终可归结为代数和逻辑的方法。而且，程序的语义及其正确性的理论基础仍然是数理逻辑，或进一步的模型论。 　　在计算机体系结构的研究中，象容错计算机系统、Transputer计算机、阵列式向量计算机、可变结构的计算机系统结构及其计算模型等都直接或间接与逻辑与代数密不可分。如容错计算机的重要基础之一是多值逻辑，Transputer计算机的理论基础是CSP理论，阵列式向量计算机必须以向量运算为基础，可变结构的计算机系统结构及其计算模型主要采用逻辑与代数的方法。 XML崭露头角，应用广泛、前景广阔 于1996年首次出现的可扩展标记语言（eXtensible Markup Language，XML），已受W3C承认并被推荐为互联网上用于数据表示以及交换的新标准，并被广泛接受，越来越多的网上资源将以XML的格式表示。XML同HTML兼容，具有平台无关性，同时又是一种真正的扩展语言，以可读的格式提供数据而又不受表现形式的限制，因此，XML的灵活、开放和基于标准的格式使它很快变成商业世界中用来交换商业数据的最广泛使用的语言，通过XML来发布数据和交换信息已被企业广泛采用。另一方面，几乎所有软件厂商都相继采用了XML技术；在网络传输协方面，由W3C、微软、IBM和SAP共同制定的简单对象访问协议（Simple Object Access Protocol，SOAP）同样也是以XML为核心。