A tableau-like proof procedure for normal modal logics

DOI10.1016/0304-3975(94)90085-XzbMath0805.03007MaRDI QIDQ1329745

Zoran Ognjanović

Publication date: 29 January 1995

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

dual clausesproof search procedureproof search tree

Mathematics Subject Classification ID

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

Related Items

Uniform and non uniform strategies for tableaux calculi for modal logics, A simple tableau system for the logic of elsewhere

Uses Software

• TABLEAUX
• PRIZ

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strategies for modal resolution: Results and problems
• Proof methods for modal and intuitionistic logics
• The programming system PRIZ
• First-order modal tableaux
• Modal resolution in clausal form
• TABLEAUX: A general theorem prover for modal logics
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Semantics-Based Translation Methods for Modal Logics
• Modal Theorem Proving: An Equational Viewpoint
• Destructive Modal Resolution
• A Machine-Oriented Logic Based on the Resolution Principle
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi