A tableau-like proof procedure for normal modal logics

DOI10.1016/0304-3975(94)90085-XMaRDI QIDQ1329745zbMATH OpenFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 3877148
• TABLEAUX: A general theorem prover for modal logics
• The recursive resolution method for modal logic
• Clausal resolution for normal modal logics
• scientific article; zbMATH DE number 4128785

Cites work

• scientific article; zbMATH DE number 4014675 (Why is no real title available?)
• scientific article; zbMATH DE number 4018413 (Why is no real title available?)
• scientific article; zbMATH DE number 4018414 (Why is no real title available?)
• scientific article; zbMATH DE number 3904560 (Why is no real title available?)
• scientific article; zbMATH DE number 3947617 (Why is no real title available?)
• scientific article; zbMATH DE number 4027426 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• scientific article; zbMATH DE number 4114588 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Destructive Modal Resolution
• First-order modal tableaux
• Modal Theorem Proving: An Equational Viewpoint
• Modal resolution in clausal form
• Proof methods for modal and intuitionistic logics
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Semantics-Based Translation Methods for Modal Logics
• Strategies for modal resolution: Results and problems
• TABLEAUX: A general theorem prover for modal logics
• The programming system PRIZ

Cited in

(5)

• Improved decision procedures for the modal logics K, T and S4
• scientific article; zbMATH DE number 3877148 (Why is no real title available?)
• A simple tableau system for the logic of elsewhere
• Uniform and non uniform strategies for tableaux calculi for modal logics
• A tableau style proof system for two paraconsistent logics

Describes a project that uses

Uses Software

• PRIZ
• TABLEAUX

This page was built for publication: A tableau-like proof procedure for normal modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1329745)