机械化定理证明研究综述

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

面向省级应急平台的突发事件案例库系统设计

突发事件案例是各种非常规突发事件发生后事件演变过程、应急处置和事后恢复与总结的真实记述。基于突发事件案例的特征和应急平台人工智能技术对案例的复用要求,根据系统工程的思想,设计了突发事件案例元模型、案例库组织模型、案例库主题词表、数据库系统及其高级应用方案。

一种新的基于假设的自然推理系统

本文在介绍自动定理证明的历史和分析自然推理研究的现有成果的基础上,提出了用以实现启发式自然推理系统HNDS的确定性推理算法。并设计了用作推理基本手段的假设机制。本系统采用知识库系统的软件结构,面向标准形式的命题逻辑和一阶谓词逻辑,对系统定理能给出清晰的类人证文过程。HNDS系统基于的推理算法理论上是合理的和完备的,这主要因为系统结合了自然推理与消解原理,并首创了量词逐层Skolem化的策略。

Prolog语言—搜索策略的归结反演推理机

Prolog语言采用一种特殊的合取范式形式来描述人工智能中所要求解的问题,这样一种知识表示方法所要求的知识推理技术必须具有机械化的可行性。要使归结过程的机械化步骤在计算机上具有可行性,还要告诉计算机一种搜索策略,即指导计算机进行归结的方法。这种方法显然是一种归纳逻辑方法。计算机中的逻辑推导既不是单纯的演绎过程,也不是单纯的归纳过程。计算机语言既是演绎的又是归纳的,是二者的融合。

刑法教义学中的类型思维

类型思维在刑法教义学中是近些年来从德国引入的一种思维方法,它不同于传统的概念思维,具有较强的分析能力和论证能力,引起我国学者的关注。然而,类型思维以其开放性,对我国传统刑法思维带来一定冲击。例如类型思维引发对刑法中的类推解释的重新认识,对禁止类推的质疑因此而生,由此形成对罪刑法定原则的动摇也并非危言耸听。在这种情况下,我们应当对类型思维进行较为深入的研究,在承认和肯定类型思维对刑法教义学理论发展所做的贡献的同时,对类型思维在刑法教义学中的适用范围加以合理限制。

个税灾害减免常态机制的构建——一种增设灾害附加扣除的进路

应对新冠疫情的税收优惠偏向于与疫情直接相关的企业纳税人,受疫情影响的自然人纳税人仅享有有限优惠。为更好地应对日后的自然灾害,宜将个税灾害减免机制常态化,但税收优惠因其缺陷而难以成为主体。灾害附加扣除更有利于实现税收法定和量能课税,财政亦可承受其成本。可参酌美国和日本的经验,以据实减免和纳税人承担协力性的申报义务作为灾害附加扣除的原则,勾勒出灾害定义、灾害损失范围、税额计算与扣除年限、纳税申报与复核等四项制度要素轮廓,并在《个人所得税专项附加扣除暂行办法》中增设专章加以规定。

带量词的合一算法

Ｒｏｂｉｎｓｏｎ于 １９６５年提出了归结原理，其主要工作是 Ｕｎｉｆｉｃａｔｉｏｎ算法。这个算法只能处理不带量词的子句公式，它不能用来发现定理的自然演绎证明。本文的算法能处理量词，它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明，基于此算法的自动自然演绎系统已实现，用它证明了Ａｎｄｒｅｗｓ；Ｂｌｅｄｓｏｅ和Ｐｅｌｌｏｔｉｅｒ挑战性问题。