Rewritings for Polarized Multiplicative and Exponential Proof Structures

We study conditions for a concurrent construction of proof-nets in the framework of linear logic following Andreoli's works. We define specific correctness criteria for that purpose. We first study the multiplicative case and show how the correctness criterion given by Danos and decidable in linear time, may be extended to closed modules (i.e. validity of polarized proof structures). We then study the exponential case and give a correctness criterion by means of a contraction relation that helps to discover frontiers of exponential boxes.     

Resolution calculus for the first order linear logic

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for the Gentzen-type system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet.     

相干命题逻辑系统R的一种演绎生成算法

本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。     

Two Natural Deduction Systems for Hybrid Logic: A Comparison

In this paper two different natural deduction systems forhybrid logic are compared and contrasted.One of the systems was originally given by the author of the presentpaper whereasthe other system under consideration is a modifiedversion of a natural deductionsystem given by Jerry Seligman.We give translations in both directions between the systems,and moreover, we devise a set of reduction rules forthe latter system bytranslation of already known reduction rules for the former system.     

Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic.     

服务组合中基于线性逻辑的消息语义匹配

介绍一种自动服务组合模型服务消息语义化匹配验证的方法。该方法先从服务描述中提取服务消息模型和服务行为模型,后将服务行为模型转换为形式化的有限状态自动机。根据有限状态自动机中的服务接口可以转化为本体概念,服务行为可以转换为线性逻辑表达式描述,使用线性逻辑的演绎方法对服务消息的匹配性和可满足性进行验证。同时,对线性逻辑的演绎定理进行适当扩展以适应服务组合的需要。     

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.     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

Linear, Branching Time and Joint Closure Semantics for Temporal Logic

Temporal logic can be used to describe processes: their behaviour ischaracterized by a set of temporal models axiomatized by a temporaltheory. Two types of models are most often used for this purpose: linearand branching time models. In this paper a third approach, based onsocalled joint closure models, is studied using models which incorporateall possible behaviour in one model. Relations between this approach andthe other two are studied. In order to define constructions needed torelate branching time models, appropriate algebraic notions are defined(in a category theoretical manner) and exploited. In particular, thenotion of joint closure is used to construct one model subsuming a setof models. Using this universal algebraic construction we show that aset of linear models can be merged to a unique branching time model.Logical properties of the described algebraic constructions are studied.The proposed approach has been successfully aplied to obtain anappropriate semantics for non-monotonic reasoning processes based ondefault logic. References are discussed that show the details of theseapplications.     

基于线性时序逻辑的实时系统模型检查

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.     

一种不确定时段的扩展时段对序逻辑：时间Petri网模型表示和线性推理

针对点－时段时序逻辑的不足,提出了一种新的时段时序逻辑－－扩展时段时序逻辑,对不确定时间段发生的事件具有较好的描述能力。时间Petri网模型表示的引入,增强了扩展时段时序逻辑的描述直观性及分析能力,为进行线性推理提供了有利的工具。同时还提出了几种变迁间的实施推理规则。运用这些规则可以简化复杂时序关系的Petri网模型,并在线性时间复杂度内定量地得到各变迁间的时序逻辑关系,因而是一种行这有效的方法。