We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfi?ability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satis?fiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfi?able input set of formulae of CMAEL(CD) and closes for every unsatisfi?able input set of formulae.
We note that there is a natural tradeoff between conceptual clarity and simplicity of (tableau-based) decision procedures on the one hand, and their technical sophistication and optimality on the other hand. We emphasize that the main objective of developing the tableau procedure presented here is the conceptual clarity, intuitiveness, and ease of implementation, rather than practical optimality. While being optimal in terms of worst-case time complexity and incorporating some new and non-trivial optimizing features (such as restricted applications of cut rules) this procedure is amenable to various improvements and further optimizations. Most important known such optimizations are techniques for elimination of bad states and tableau methods developed for some related logics in @cite_23 , @cite_39 and versions of tableau as in @cite_39 for , @cite_30 for PDL with converse operators, @cite_41 for the description logic SHI and of sequent calculi, in @cite_42 for and in @cite_26 for LTL and CTL. We discuss briefly the possible modifications of our procedure, implementing such optimizing techniques in Section .
@cite_30 @cite_26 @cite_41 @cite_42 @cite_39 @cite_23
2949377023 2047456744 2515200 1527982431
We give an optimal (EXPTIME), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound methodto combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL. Abstract Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics. We give the first cut-free ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHI, which extends the description logic ALC with transitive roles, inverse roles and role hierarchies. The paper presents a one-pass tableau calculus PLTLT for the propositional linear time logic PLTL. The calculus is correct and complete and unlike in previous decision methods, there is no second phase that checks for the fulfillment of the so-called eventuality formulae. This second phase is performed locally and is incorporated into the rules of the calculus. Derivations in PLTLT are cyclic trees rather than cyclic graphs. When used as a basis for a decision procedure, it has the advantage that only one branch needs to be kept in memory at any one time. It may thus be a suitable starting point for the development of a parallel decision method for PLTL.