A tableau-like proof procedure for normal modal logics

DOI10.1016/0304-3975(94)90085-XzbMATH Open0805.03007MaRDI QIDQ1329745FDOQ1329745

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)

Cites Work

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

Cited In (4)

• Improved decision procedures for the modal logics K, T and S4
• 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

Uses Software

• TABLEAUX
• PRIZ

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)