A Sequent Calculus for Propositional Dynamic Logic for Agents

We consider propositional dynamic logic for agents. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.     

命题逻辑公式的压缩表示及其相应的形式系统

提出一种将命题逻辑公式压缩表示的方法--公式的压缩图,给出相应的形式系统,并证明该系统的证明效率比传统相继式演算系统Gentzen\{cut}有指数级的提高,从而为命题逻辑提供了一种新的有效的推理系统.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

A proof-search procedure for intuitionistic propositional logic

A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.     

A Sequent Calculus for Propositional Dynamic Logic for Agents with Interactions

We consider a propositional dynamic logic for agents with interactions such as known commitment, no learning, and perfect recall. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 2, pp. 261–269, April–June, 2005.     

Efficient loop-check for KD 45 logic

We introduce a new sequent calculus for KD 45 logic. A loop-check technique is used to determine whether a sequent derivable or not. We concentrate ourselves on the efficiency of the loop-check technique used. The efficiency is obtained by making the loop-check to act locally (then we need to check only one or two current sequents), instead of a global loop-check used in known works as [3]. Moreover, the sequent calculus introduced uses a marked operator □ to integrate loop-check into an inference rule. Besides the efficient loop-check used, the sequent calculus introduced produces smaller derivation trees that reduce the derivation time. We also prove a lemma which determines the maximal number of modality rule applications in one branch of a tree. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 1, pp. 55–66, January–March, 2006.     

On temporal logic S4Dbr

In this paper, we study the temporal logic S4Dbr with two temporal operators “always” and “eventually.” An equivalent sequent calculus is presented with formulae as modal clauses or modal clauses starting with operator “always.” An upper bound of deduction tree is given for propositional logic. A theorem prover for propositional logic is written in SWI-Prolog. Published in LietuvosMatematikos Rinkinys, Vol. 46, No. 2, pp. 203–214, April–June, 2006.     

PSPACE complexity of modal logic <Emphasis Type="Italic">K D</Emphasis>45<Subscript>n</Subscript>

We study sequent calculus for multi-modal logic K D45_n and its complexity. We introduce a loop-check free sequent calculus. Loop-check is eliminated by using the marked modal operator □_i^•, which is used as an alternative to sequents with histories ([8], [3], [5]). All inference rules are invertible or semi-invertible. To get this, we use or branches beside common and branches. We prove the equivalence between known sequent calculus and our newly introduced efficient sequent calculus. We concentrate on the complexity analysis of the introduced sequent calculus for multi-modal logic K D45_n. We prove that the space complexity of the given calculus is polynomial (O(l ³)). We show the maximum height of the constructed derivation tree that leads to the reduction of the time and space complexity. We present a decision algorithm for multi-modal logic K D45_n and some nontrivial examples to improve the introduced loop-check free sequent calculus.     

Local computation in linear logic

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.     

Proof complexity of propositional default logic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen??s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti??s enhanced calculus for skeptical default reasoning.     

Sequent calculi for propositional star-free likelihood logic

We consider classical, multisuccedent intuitionistic, and intuitionistic sequent calculi for propositional likelihood logic. We prove the admissibility of structural rules and cut rule, invertibility of rules, correctness of the calculi, and completeness of the classical calculus with respect to given semantics.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 1, pp. 3–21, January–March, 2005.     

A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.     

Proof analysis in intermediate logics

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the G?del–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.     

Proofs and Countermodels in Non-Classical Logics

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope.     

Distributive-Lattice Semantics of Sequent Calculi with Structural Rules

The goal of the paper is to develop a universal semantic approach to derivable rules of propositional multiple-conclusion sequent calculi with structural rules, which explicitly involve not only atomic formulas, treated as metavariables for formulas, but also formula set variables (viz., metavariables for finite sets of formulas), upon the basis of the conception of model introduced in (Fuzzy Sets Syst 121(3):27–37, 2001). One of the main results of the paper is that any regular sequent calculus with structural rules has such class of sequent models (called its semantics) that a rule is derivable in the calculus iff it is sound with respect to each model of the semantics. We then show how semantics of admissible rules of such calculi can be found with using a method of free models. Next, our universal approach is applied to sequent calculi for many-valued logics with equality determinant. Finally, we exemplify this application by studying sequent calculi for some of such logics.      

A fuzzy logic for an ordinal sum t-norm

Among the class of residuated fuzzy logics, a few of them have been shown to have standard completeness both for propositional and predicate calculus, like Gödel, NM and monoidal t-norm-based logic systems. In this paper, a new residuated logic NMG, which aims at capturing the tautologies of a class of ordinal sum t-norms and their residua, is introduced and its standard completeness both for propositional calculus and for predicate calculus are proved.     

中介命题演算系统$MP^{M}$的代数系统

MP~M系统是在中介逻辑系统的基础上建立起来的,用于处理数据库中不完全信息的三值逻辑命题演算系统．本文通过在MP~M系统上建立一个代数系统,对MP~M系统进行了代数抽象,讨论了MP~M系统的代数性质．本文还研究了该代数系统的次直积,以及与其它一些代数系统之间的关系．     

Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

A saturated calculus for the so-called Horn-like sequents of a complete class of a linear temporal logic of the first order is described. The saturated calculus contains neither induction-like postulates nor cut-like rules. Instead of induction-like postulates the saturated calculus contains a finite set of “saturated” sequents, which (1) capture and reflect the periodic structure of inductive reasoning (i.e., a reasoning which applies induction-like postulates); (2) show that “almost nothing new” can be obtained by continuing the process of derivation of a given sequent; (3) present an explicit way of generating the so-called invariant formula in induction-like rules. The saturated calculus for Horn-like sequents allows one: (1) to prove in an obvious way the completeness of a restricted linear temporal logic of the first order; (2) to construct a computer-aided proof system for this logic; (3) to prove the decidability of this logic for logically decidable Horn-like sequents. Bibliography: 15 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 123–144. Translated by R. Pliuškevičius.     

Some decidable classes of formulas of pure hybrid logic

We consider the formulas of pure hybrid logic without occurrences of a satisfaction operator. We describe a couple of formula derivation tactics in sequent calculus and prove the decidability of two classes of formulas. Decidable classes are obtained by setting restrictions on nominal occurrences in the formulas. Published in Lietuvos Matematikos Rinkinys, Vol. 44, No. 4, pp. 563–572, October–December, 2007.     

On transformations of constant depth propositional proofs

This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.