Free-Variable Tableaux for Propositional Modal Logics |
| |
| Authors: | Bernhard Beckert Rajeev GorÉ |
| |
| Affiliation: | (1) Inst. for Logic, Complexity and Deduction Systems, University of Karlsruhe, D-76128 Karlsruhe, Germany;(2) Automated Reasoning Project, Australian National University, Canberra, ACT, 0200, Australia |
| |
| Abstract: | Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux. |
| |
| Keywords: | automated deduction modal logics modal theorem proving free-variable tableaux |
| 本文献已被 SpringerLink 等数据库收录！ |
|
