Proof strategies in linear logic

Linear logic, introduced by J.-Y. Girard, is a refinement of classical logic providing means for controlling the allocation of resources. It has aroused considerable interest from both proof theorists and computer scientists. In this paper we investigate methods for automated theorem proving in propositional linear logic. Both the bottom-up (tableaux) and top-down (resolution) proof strategies are analyzed. Various modifications of sequent rules and efficient search strategies are presented along with the experiments performed with the implemented theorem provers.     

A clausal resolution method for branching-time logic ECTL+

We expand the applicability of the clausal resolution technique to the branching-time temporal logic ECTL⁺. ECTL⁺ is strictly more expressive than the basic computation tree logic CTL and its extension, ECTL, as it allows Boolean combinations of fairness and single temporal operators. We show how any ECTL⁺ formula can be translated to a normal form the structure of which was initially defined for CTL and then used for ECTL. This enables us to apply to ECTL⁺ a resolution technique defined over the set of clauses. Both correctness of the method and complexity of the transformation procedure are given.     

The conjoinability relation in Lambek calculus and linear logic

In 1958 J. Lambek introduced a calculusL of syntactic types and defined an equivalence relation on types: x y means that there exists a sequence x=x₁,...,x_n=y (n 1), such thatx _i x _i+1 or x_i+ x _i (1 i n). He pointed out thatx y if and only if there is joinz such thatx z andy z. This paper gives an effective characterization of this equivalence for the Lambeck calculiL andLP, and for the multiplicative fragments of Girard's and Yetter's linear logics. Moreover, for the non-directed Lambek calculusLP and the multiplicative fragment of Girard's linear logic, we present linear time algorithms deciding whether two types are equal, and finding a join for them if they are.The author was sponsored by project NF 102/62-356 (Structural and Semantic Parallels in Natural Languages and Programming Languages), funded by the Netherlands Organization for the Advancement of Research (N.W.O.).     

On structuring proof search for first order linear logic

Full first-order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the ‘proof search as computation’ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first-order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.     

A Matrix Characterization for Multiplicative Exponential Linear Logic

We develop a matrix characterization of logical validity in MELL, the multiplicative fragment of propositional linear logic with exponentials and constants. To prove the correctness and completeness of our characterization, we use a purely proof-theoretical justification rather than semantical arguments. Our characterization is based on concepts similar to matrix characterizations proposed by Wallen for other nonclassical logics. It provides a foundation for developing proof search procedures for MELL by adopting techniques that are based on these concepts and also makes it possible to adopt algorithms that translate the machine-found proofs back into the usual sequent calculus for MELL.     

Decidability by Resolution for Propositional Modal Logics

The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalization, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimized functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, many standard first-order theorem provers that are based on resolution are suitable for facilitating modal reasoning.     

Autoepistemic logic of first order and its expressive power

We study the expressive power of first-order autoepistemic logic. We argue that full introspection of rational agents should be carried out by minimizing positive introspection and maximizing negative introspection. Based on full introspection, we propose the maximal well-founded semantics that characterizes autoepistemic reasoning processes of rational agents, and show that breadth of the semantics covers all theories in autoepistemic logic of first order, Moore's AE logic, and Reiter's default logic. Our study demonstrates that the autoepistemic logic of first order is a very powerful framework for nonmonotonic reasoning, logic programming, deductive databases, and knowledge representation.This research is partially supported by NSERC grant OGP42193.     

基于一阶逻辑的GIService服务发现

针对GIService服务发现,提出了基于一阶逻辑的GIService服务描述与匹配方法。使用一阶逻辑工具描述服务接口、运行条件和程序逻辑等GIService特征,提出基于描述逻辑与霍尔规则相似度计算的GIService服务匹配方法。实验案例证明,基于一阶逻辑的GIService服务发现可以全面表达GIService特征,得到更加准确的服务匹配结果。     

Strong normalization property for second order linear logic

The paper contains the first complete proof of strong normalization (SN) for full second order linear logic (LL): Girard’s original proof uses a standardization theorem which is not proven. We introduce sliced pure structures (sps), a very general version of Girard’s proof-nets, and we apply to sps Gandy’s method to infer SN from weak normalization (WN). We prove a standardization theorem for sps: if WN without erasing steps holds for an sps, then it enjoys SN. A key step in our proof of standardization is a confluence theorem for sps obtained by using only a very weak form of correctness, namely acyclicity slice by slice. We conclude by showing how standardization for sps allows to prove SN of LL, using as usual Girard’s reducibility candidates.     

A calculus for four-valued sequential logic

We present a complete axiomatisation for four-valued sequential logic. It consists of nine axioms, from which all valid laws can be derived by equational reasoning. These nine axioms are independent of each other.     

命题演算两个推理系统的等价性

首先介绍命题演算的Gentzen型系统G,然后给出一个命题演算的永真推理系统H,最后证明一个命题在G中可证当且仅当它在H中可证,从而G与H是等价的.     

The saturated tableaux for linear miniscoped horn-like temporal logic

A new type of tableau system is proposed for the complete class (called miniscoped Horn-like) of first-order linear temporal logic. The described system instead of induction-like postulates contains some nonlogical axioms indicating the saturation of a derivation process in this system.     

Inductive expansion: A calculus for verifying and synthesizing functional and logic programs

Guarded Horn clauses over a many-sorted polymorphic signature provide a powerful syntax for design specifications. Expressed as a set of positive Gentzen clauses with a common guard, requirements to such a specification can be proved top-down by inductive expansion: conclusions and generators of the clauses are transformed via resolution and paramodulation upon axioms, lemmas and induction hypotheses into the guard. Case distinctions are generated when axioms or lemmas are applied in parallel. They split the proof into subexpansions, which are later rejoined by applying disjunctive lemmas. Induction orderings need not be selected before redices for induction hypotheses have been created.The controlled expansion of requirements to a function (or predicate) may produce axioms representing a program for that function. This generalizes traditional approaches to program synthesis such as fold& unfold, divide&conquer or deductive tableaus. Ground confluent and strongly terminating design specifications yield decidable criteria for constructors and unsolvable goals and thus reduce the search space of inductive expansion.     

面向事实建模方法ORM的一阶逻辑形式化分析

对象角色建模方法ORM是一种完全面向交流的面向事实概念建模方法,目前已发展到2.0版,已应用于本体论工程,因此需要对其进行形式化以分析其本体表达能力。Halpin定义了一种知识表达语言KL,并使用KL形式化分析了早期版本的ORM。本文借鉴Halpin的研究成果,采用经典的一阶逻辑语言L 全面地分析了ORM 2.0的形式化语义。     

Class Based Contextual Logic for DOOD

Cntextual logic provides a mechanism to reason about modules.In this paper,this theory of modules if modules is extended to a context theory of classes where class is in the true spirit of object-oriented databases.The logic,referred to as CLOG,is class-based.CLOG supports class,object identity,multiple role of object, monotonic and non-monotonic inheritance of data and method,method factoring,views,derived and query classes.Views and derived classes are queries in themselves.Objects are pure data terms representing the ground instances of facts in the class.Object identity is a first class term in the logic.Inheritance is handled through delegation.     

格值命题逻辑系统L9P(X)中的自动推理算法

给出了格值命题逻辑系统L₉P（X）上的放缩原理和放缩归结原理,基于放缩归结原理,给出了一种判断L₉P（X）上子句集S为M－可满足的自动推理算法（这里M为L₉上的中界元）,并证明了其可靠性和完备性。     

On decidability and model checking for a first order modal logic for value-passing processes

A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.     

相干命题逻辑自然推理系统NR的自动证明*

给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理。