Evaluating Optimized Decision Procedures for Propositional Modal K (m) Satisfiability

Heavily optimized decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC, are tested on randomly generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.     

Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m)

The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we consider satisfiability in modal K(m), that is modal K with m modalities, and develop an algorithm, called K , on top of an implementation of the Davis–Putnam–Longemann–Loveland procedure. K is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system K . The experimental results show that K outperforms K and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m).     

动态描述逻辑的Tableau判定算法

动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.     

Deciding Regular Grammar Logics with Converse Through First-Order Logic

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF², which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF² include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF² without extra machinery such as fixed-point operators.     

Generalized modal satisfiability

It is well known that modal satisfiability is PSPACE-complete (Ladner (1977) [21]). However, the complexity may decrease if we restrict the set of propositional operators used. Note that there exist an infinite number of propositional operators, since a propositional operator is simply a Boolean function. We completely classify the complexity of modal satisfiability for every finite set of propositional operators, i.e., in contrast to previous work, we classify an infinite number of problems. We show that, depending on the set of propositional operators, modal satisfiability is PSPACE-complete, coNP-complete, or in P. We obtain this trichotomy not only for modal formulas, but also for their more succinct representation using modal circuits. We consider both the uni-modal and the multi-modal cases, and study the dual problem of validity as well.     

A polynomial space construction of tree-like models for logics with local chains of modal connectives

The LA-logics (“logics with Local Agreement”) are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov's logic DALLA and Nakamura's logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively.     

Using Resolution for Testing Modal Satisfiability and Building Models

This paper presents a translation-based resolution decision procedure for the multimodal logic K _(m)(,,) defined over families of relations closed under intersection, union, and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures that are based on ordering refinements, our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and as a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.     

On the computational complexity of satisfiability in propositional logics of programs

The satisfiability problems of propositional algorithmic logic and propositional dynamic logic are shown to be complete in the classes of languages accepted in polynomial space by the deterministic and alternating Turing machines respectively. Explicit upper and lower bounds on the space complexity are calculated. Exponential lower bounds on the space complexity of the satisfiability problems of these logics extended by adding a certain program connective are proved.     

Labelled Modal Logics: Quantifiers

In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this approach to quantified modal logics, providing formalizations for logics with varying, increasing, decreasing, or constant domains. The result is modular with respect to both properties of the accessibility relation in the Kripke frame and the way domains of individuals change between worlds. Our approach has a modular metatheory too; soundness, completeness and normalization are proved uniformly for every logic in our class. Finally, our work leads to a simple implementation of a modal logic theorem prover in a standard logical framework.     

标记模态归结的推广

本文将作者提出的高效的命题模态Ｄ逻辑的标记模态归结方法推广到了命题模态逻辑Ｋ,Ｋ４,Ｄ４,Ｔ,Ｓ４系统,建立了上述命题模态逻辑的标记归结形式系统ＭＲＫ,ＭＲＫ４,ＭＲＤ４,ＭＲＴ,ＭＲＳ４,并用转移子句模式的方法,借助于标记模态归结对命题模态Ｄ逻辑的可靠性结果,证明了标记模态归结系统ＭＲＫ,ＭＲＫ４,ＭＲＤ４,ＭＭＲＴ,ＭＲＳ４分别关于命题模式逻辑Ｋ,Ｋ４、Ｄ４,Ｔ,Ｓ４的可靠性,进而得到了它们的     

模态逻辑推理的翻译方法

文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性，还给出了一些试验结果，说明该方法实际可行的。     

Bounded Model Checking of CTL^*

Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.     

Filter-based resolution principle for lattice-valued propositional logic LP(X)

As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.     

TABLEAUX: A general theorem prover for modal logics

We present a general theorem proving system for propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since it provides an unified environment for various kinds of modal operators and for a wide class of modal logics, including usual temporal, epistemic or dynamic logics. We survey the modal languages covered by TABLEAUX, which range from the basic one L(, ) through a complex multimodal language including several families of operators with their transitive-closure and converse. The decision procedure we use is basically a semantic tableaux method, but with slight modifications compared to the traditional one. We emphasize the advantages of such semantical proof methods for modal logics, since we believe that the models construction they provide represents perhaps the most attractive feature of these logics for possible applications in computer science and AI. The system has been implemented in Prolog, and appears to be of reasonable efficiency for most current examples. Experimental results are given in the paper, with two lists of test examples.A preliminary version of this paper appeared in the Proceedings of the International Computer Science Conference (ICSC'88), Hong-Kong, December 19–21, 1988.     

Clausal resolution in a logic of rational agency

A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief ). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given.     

Many-valued logic and mixed integer programming

We generalize prepositional semantic tableaux for classical and many-valued logics toconstraint tableaux. We show that this technique is a generalization of the standard translation from CNF formulas into integer programming. The main advantages are (i) a relatively efficient satisfiability checking procedure for classical, finitely-valued and, for the first time, for a wide range of infinitely-valued propositional logics; (ii) easy NP-containment proofs for many-valued logics. The standard translation of two-valued CNF formulas into integer programs and Tseitin's structure preserving clause form translation are obtained as a special case of our approach.Part of the research reported here was carried out while the author was supported by a grant within the DFG Schwerpunktprogramm Deduktion. Preliminary and partial versions of this paper were published as [15, 16].     

Invariant-Free Clausal Temporal Resolution

Resolution is a well-known proof method for classical logics that is well suited for mechanization. The most fruitful approach in the literature on temporal logic, which was started with the seminal paper of M. Fisher, deals with Propositional Linear-time Temporal Logic (PLTL) and requires to generate invariants for performing resolution on eventualities. The methods and techniques developed in that approach have also been successfully adapted in order to obtain a clausal resolution method for Computation Tree Logic (CTL), but invariant handling seems to be a handicap for further extension to more general branching temporal logics. In this paper, we present a new approach to applying resolution to PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Hence, we say that the approach presented in this paper is invariant-free. Our method is based on the dual methods of tableaux and sequents for PLTL that we presented in a previous paper. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called trs-resolution, that extends classical propositional resolution. Finally, we prove that trs-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL.     

Branching-Time Logics Repeatedly Referring to States

While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism, hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics. As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be 2EXPTIME-complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability for NCTL* has nonelementary complexity.