共查询到20条相似文献,搜索用时 15 毫秒
1.
Proof Nets for Classical Logic 总被引:1,自引:0,他引:1
2.
We explain Stålmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification. 相似文献
3.
Extended IF 逻辑是一阶逻辑的扩张,其主要特点是可表达量词间的相互依赖和独立关系,但其命题部分至今没有得到公理化.基于Cirquent 演算方法,给出了一个关于Cirquent 语义(命题水平)可靠完备的形式系统.该系统能够很好地解释和表达命题联结词间的相互依赖和独立关系,从而使Extended IF 逻辑在命题水平得到了真正意义上的公理化. 相似文献
4.
A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems. 相似文献
5.
Many proof search strategies can be expressed as restrictions on the order of application of the rules of the sequent calculus. Properties of these strategies are then shown by permutation arguments, such as showing that a given strategy is complete by transforming an arbitrary proof into one which obeys the strategy. Such analyses involve some very tedious manipulations of proofs, and are potentially overwhelming for humans. In this paper we investigate the development of systematic techniques for the analysis of sequent calculi. We show how a particular specification of inference rules leads to a detailed analysis of permutation properties for these rules, and we also investigate how to detect redundancies in proofs resulting from these rules. 相似文献
6.
Uniform Provability in Classical Logic 总被引:1,自引:0,他引:1
7.
8.
In this paper we study a version of constructive linear-time temporal logic (LTL) with the “next” temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time analysis via the Curry-Howard isomorphism. However, he did not investigate the logic itself in detail; he has proved only that the logic augmented with negation and classical reasoning is equivalent to (the “next” fragment of) the standard formulation of classical linear-time temporal logic. We give natural deduction, sequent calculus and Hilbert-style proof systems for constructive LTL with conjunction, disjunction and falsehood, and show that the sequent calculus enjoys cut elimination. Moreover, we also consider Kripke semantics and prove soundness and completeness. One distinguishing feature of this logic is that distributivity of the “next” operator over disjunction “?(A∨B)⊃?A∨?B” is rejected in view of a type-theoretic interpretation. 相似文献
9.
10.
We propose an extension of the propositional proof logic languageby the second-order variables denoting the reference constructors(like the formula which is proven by x). The prooflogic in this weak second-order language is axiomatized viathe calculus ref, the (Functional)Logic of Proofs with References. It is supplied with the formalarithmetical semantics: we prove that ref is sound with respect to arithmetical interpretationsand is a conservative extension of propositional single-conclusionproof logic . Finally,we demonstrate how the language of ref can be used as a scheme language for arithmetic and providethe corresponding proof conversion method. 相似文献
11.
本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。 相似文献
12.
13.
This paper studies a restricted version of the ambient calculus. We only allow single-threaded ambients migrating in a network of immobile ambients, exchanging payloads, and delivering them. With this restriction, we arrive at a calculus free from grave interferences. In previous works, this is only possible by sophisticated type systems.We focus on the expressiveness of the restricted calculus. We show that we can still repeat Zimmer's encoding of name-passing in our calculus. Moreover, we prove a stronger operational correspon- dence result using a novel spatial logic, which specifies spatial properties of processes invariant to process reductions. 相似文献
14.
15.
In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. 相似文献
16.
Differential Dynamic Logic for Hybrid Systems 总被引:2,自引:0,他引:2
André Platzer 《Journal of Automated Reasoning》2008,41(2):143-189
Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions
and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation
for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation
for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus
with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic
to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts.
Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential
equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our
calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics. 相似文献
17.
在基于命题逻辑的可满足性问题(SAT)求解器和基于一阶逻辑的定理证明器上,子句集简化一直是必不可少的步骤,而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法(RHTE)和归结隐藏包含消去方法(RHSE)提升到一阶逻辑上,并且利用蕴含模归结原则(IMR)证明了这种提升方式在一阶逻辑上具有可靠性(Soundness),即依据这两种子句消去方法删除一阶逻辑公式集中的子句,并不会改变公式集的可满足性或者不可满足性。此外,将这两个方法与一阶逻辑子句消去方法锁子句消去方法(BCE)和归结包含消去方法(RSE)进行组合推广,发展得到一阶逻辑上新型子句消去方法(BC+RHS)E、(RS+RHT)E和(RHS+RHT)E,并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后,分析比较了这些子句消去方法的有效性,并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。 相似文献
18.
19.
以一阶谓词逻辑为基础,讨论约束满足问题.着重研究一阶逻辑公式可满足性的局部搜索法,并与命题逻辑中的可满足性过程加以比较.以皇后问题和哈密顿回路问题为例,说明基于一阶逻辑的方法能处理较大的问题实例. 相似文献
20.
本文针对复杂工业对象智能控制系统中建立模糊逻辑系统的表格查询法进行改进,讨论了改进的表格查询法的计算过程,分析了仿真结果和提高模糊逻辑系统精度的方法。 相似文献