Uniform and non uniform strategies for tableaux calculi for modal logics

DOI10.1080/11663081.1995.10510844zbMath0826.03006OpenAlexW2005146745MaRDI QIDQ4835516

Stéphane P. Demri

Publication date: 28 November 1995

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.1995.10510844

zbMATH Keywords

automated reasoningheuristicpropositional modal logicsbacktrackingtableaux systemsordering strategies

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items

Complexity of hybrid logics over transitive frames, A simple tableau system for the logic of elsewhere, A new method for testing decision procedures in modal logics, EXPtime tableaux for ALC

Uses Software

• TPTP
• Minlog

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal tableau calculi and interpolation
• Strategies for modal resolution: Results and problems
• Proof methods for modal and intuitionistic logics
• First-order modal tableaux
• Application of modal logic to programming
• TABLEAUX: A general theorem prover for modal logics
• A tableau-like proof procedure for normal modal logics
• Binary closure-algebraic operations that are functionally complete
• Note on G.J. Massey's closure-algebraic operation
• Nonmonotonic Logic II
• Methods for Automated Theorem Proving in Nonclassical Logics
• Some theorems about the sentential calculi of Lewis and Heyting