一般结构语义下限定的完备性与可满足性

本文提出用一般结构极小模型解释限定公理,并证明在此语义下,二阶限定是完备的.此外,作者还把Mott的非速归闭限定引入二阶限定,证明在一般结构语义下,二阶非递归闭限定是可满足的.     

逻辑语言Setlog的证明论和过程性语义

本文对目前在处理复杂对象上的３种有代表性的逻辑语言进行了详细的综合分析，对比了它们在语法，语义及应用上的优优点。在此基础上提出了一种清晰，严谨和可实现的、能处理复杂对象的逻辑语言Ｓｅｔｌｏｇ。本文给出了Ｓｅｔｌｏｇ语言的严谨法形式，并讨论了模型论和证明论。     

法律知识的因果表达和非单调推理模型

1 引言计算机在法律业务上的辅助应用总的来说可分为两类;计算机辅助法律条文查询系统和面向案例的计算机辅助法律分析与解释系统.计算机辅助法律条文查询系统的目标是建立一个丰富的法律条文和案例库,并对它们进行分类,建立索引,通过智能搜索引擎供法律专业人员和普通人查询有关法律条文或案例。法律文件繁复、浩大,依赖人脑记忆可靠性差,手工查找则费工费时,计算机正可以发挥其记忆量、查找迅速等特点。所以这方面的应用是比较成功的,例如北京大学开发的法律查询系统。一个面向案例的计算机辅助法律分析与解释系统能够根据系统中已有的法律知识(包括法律条文和案例)对实际案例进行分析和解释,并提出建设性的法律建议或结论以供人们参考。与计算机辅助法律条文查询系统相比,计算机辅助法律分析与解释系统需要运用法律知识进行推理,实际上是一个专家咨询系统。建立合理有效的法律知识的表达方法与推理机制是构造一个法律专家咨询系统的关键,这项任务是非常困难的。因为法律知识不仅仅是指成文的法律条文,还应该包括大量的法律解释、判例、不成文的法律规定等等,     

简洁非交互零知识证明综述

区块链、隐私计算、人工智能等技术的快速发展,极大地推动了对零知识证明尤其是简洁非交互零知识证明的研究.本文从通用构造方法、底层技术原理、协议性能表现、安全性等角度深入研究了现有的简洁非交互零知识证明.首先,总结了简洁非交互零知识证明的通用构造方法.其次,分别基于信息论安全证明和底层关键技术对现有的简洁非交互零知识证明进行分类并提炼了核心思路,深入分析了典型协议的实现原理.再次,辨析了各类协议的性能表现,探讨其安全性并指出其适用场景.最后,总结了简洁非交互零知识证明的研究热点和发展方向.     

一般术语公理下的模糊描述逻辑FALCN推理

分析了一般术语公理下推理的主要难点:在模糊解释中的隶属度不是离散值,而是区间[0,1]上的连续值.为解决该难点,提出了模糊描述逻辑FALCN下的模糊解释离散化方法,从而使解释中的隶属度都属于一个特殊的有限离散集合.基于该离散化方法,给出一般术语公理下FALCN推理问题的离散Tableau推理技术,包括离散Tableau的定义以及离散Tableau的构造算法,并证明了算法的正确性、完备性和复杂度.     

基于范畴论的形式语言模型建模方法研究

形式语言模型转换的语义一致性与其形式系统完备性分析是当前形式语言理论尚未有效解决的难题。针对形式语言模型的应用需求与研究现状,建立形式文法模型及其形式语言模型,应用范畴论方法构建具有普适意义的形式文法模型范畴与形式语言模型范畴。在形式语言族模型的形式化理论框架内,用与特定形式语言无关的范畴论方法研究形式语言模型转换的语义一致性。初步分析形式系统的完备性,通过与形式语言理论主要研究方法的比对论证了范畴论方法的优势,为形式语言模型的范畴论方法研究提供一个便利、高效的形式化理论框架。     

随机归约的五步完美零知识证明系统*

构造了一个完美零知识的五步交互证明系统,该系统不依赖于任何(复杂性和计算能力)假设, 在该系统中,证明者可具有有限或无限的计算能力.     

一个基于零知识证明的非否认电子现金方案

大多电子现金具有匿名性特点以保证所有者的私有性,可是很少有电子现金具有非否认特点。电子现金具有非否认性很有必要,它能避免由于现金敲诈、洗钱、抢劫被盗、丢失、错误使用、重复花费等带来的损失。基于部分盲签名和零知识证明,设计了一个同时具有匿名性和非否认的电子现金。     

标准模型下可证明安全的新公钥加密方案

针对标准模型下抗适应性选择密文攻击语义安全的公钥加密方案存在的效率比较低或者所基于的计算假设比较强的问题,基于最近提出的d-判定性Diffie-Hellman问题构造了一个新的可证明安全的公钥加密方案。方案的构造和安全性证明采用哈希证明系统方法,达到了高效安全的目标。方案所基于的d-判定性Diffie-Hellman问题的难度介于计算Diffie-Hellman问题和判定性Diffie-Hellman问题之间,方案的效率优于基于计算Diffie-Hellman问题的方案,与基于判定性Diffie-Hellman问题的方案相近。该方案实现了计算假设与效率之间的一个比较好的折中,并且可以根据实际需要选择不同的d值以达到不同的安全级别。     

Uniform Closures: Order-Theoretically Reconstructing Logic Program Semantics and Abstract Domain Refinements

The notion of uniform closure operator is introduced, and it is shown how this concept surfaces in two different areas of application of abstract interpretation, notably in semantics design for logic programs and in the theory of abstract domain refinements. In logic programming, uniform closures permit generalization, from an order-theoretic perspective, of the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the model-theoretic characterization of the well-known s-semantics using pure order-theoretic concepts only. As far as the systematic refinement operators on abstract domains are concerned, we show that uniform closures capture precisely the property of a refinement of being invertible, namely of admitting a related operator that simplifies as much as possible a given abstract domain of input for that refinement. Exploiting the same argument used to reconstruct the s-semantics of logic programming, we yield a precise relationship between refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

基于分离逻辑的程序验证研究综述

上世纪60-70年代以来,虽然有Floyd-Hoare逻辑的出现,但是使用形式化工具对命令式程序的正确性和可靠性进行自动验证一直被认为是极具挑战性、神圣不可及的工作.上世纪末由于更多的科研投入,特别是微软、IBM等大型公司研发部门的大量人力物力的投入,程序验证方面在本世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRÉE工具,用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆（Heap）：ASTRÉE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是个难题.2001-2002年分离逻辑（separation logic）提出后,其分离（separation）思想和相应的框（frame）规则使得局部推理（local reasoning）可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如SpaceInvader/Abductor、Slayer、HIP/SLEEK、CSL等工作.本文将着重对这方面的部分重要工作进行阐述.     

Deriving Proof Rules from Continuation Semantics

We claim that a continuation style semantics of a programming language can provide a starting point for constructing its proof system. The basic idea is to see weakest preconditions as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples {p} C {r}) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations. Received July 1997 / Accepted in revised form August 1999     

The Rewriting Logic Semantics Project

Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact that a rewrite theory's axioms include both equations and rewrite rules provides a very useful “abstraction knob” to find the right balance between abstraction and observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.     

Proof Systems for Planning Under Cautious Semantics

Planning with incomplete knowledge becomes a very active research area since late 1990s. Many logical formalisms introduce sensing actions and conditional plans to address the problem. The action language $\mathcal{A}_{K}$ invented by Son and Baral is a well-known framework for this purpose. In this paper, we propose so-called cautious and weakly cautious semantics for $\mathcal{A}_{K}$ , in order to allow an agent to generate and execute reliable plans in safety-critical environments. Intuitively speaking, cautious and weakly cautious semantics enable the agent to know exactly what happens after the execution of an action. Computational complexity analysis shows that cautious semantics reduces the reasoning complexity of $\mathcal{A}_{K}$ , it is also worth to point out that many useful domains could still be expressed with this setting. Another important contribution of our work is the development of Hoare style proof systems. These proof systems are served as inference mechanisms for the verification of conditional plans, and proved to be sound and complete. In addition, they could also be used for plan generation, in the sense that constructing a derivation is indeed a procedure to finding a plan. We point out that the proof systems posses a nice property for off-line planning, that is, the agent could generate and store short proofs in her spare time, and perform quick plan query by easily constructing a long proof from the stored shorter ones (under the assumption that sufficient proofs are stored).