摘要: Single Step Tableaux (SST) are the basis of a calculus for modal logics that combines different features sequent and prefixed tableaux into simple, modular, strongly analytic, effective wide range logics. The paper presents number computational results about SST (confluence, decidability, space complexity, modularity, etc.) compares with other formalisms such as translation methods, resolution, Gentzen-type tableaux. For instance, it discusses feasibility infeasibility deriving decision procedures translation-based methods by replacing loop checking techniques simpler termination checks. The complexity searching validity logical consequence is discussed. Minimal conditions on search strategies proven to yield Pspace (and NPtime S5 KD45) procedures. The also methodology underlying construction correctness completeness proofs.
springer.com
amu.edu.pl 
sci-hub.se 参考文章(43)
Fabio Massacci, Contextual reasoning is NP-complete national conference on artificial intelligence. pp. 621- 626 ,(1996)
Alessandra Russo, Generalising Propositional Modal Logic Using Labelled Deductive Systems frontiers of combining systems. pp. 57- 73 ,(1996) , 10.1007/978-94-009-0349-4_2
Bernhard Beckert, Rajeev Goré, Free Variable Tableaux for Propositional Modal Logics theorem proving with analytic tableaux and related methods. pp. 91- 106 ,(1997) , 10.1007/BFB0027407
Renate A. Schmidt, Resolution is a decision procedure for many propositional modal logics advances in modal logic. pp. 189- 208 ,(1997)
Ullrich Hustadt, Renate A. Schmidt, On evaluating decision procedures for modal logic international joint conference on artificial intelligence. pp. 202- 207 ,(1997)
Alain Heuerding, Michael Seyfried, Heinrich Zimmermann, Efficient Loop-Check for Backward Proof Search in Some Non-classical Propositional Logics theorem proving with analytic tableaux and related methods. pp. 210- 225 ,(1996) , 10.1007/3-540-61208-4_14
Melvin Fitting, Basic modal logic Handbook of logic in artificial intelligence and logic programming (vol. 1). pp. 368- 448 ,(1993)
Raymond M. Smullyan, First-Order Logic ,(1968)
Ullrich Hustadt, Renate A. Schmidt, On Evaluating Decision Procedures for Modal Logics Untitled Event. pp. 202- 207 ,(1997)
Giuseppe Giacomo, Fabio Massacci, Tableaux and Algorithms for Propositional Dynamic Logic with Converse conference on automated deduction. pp. 613- 627 ,(1996) , 10.1007/3-540-61511-3_117