Modal resolution in clausal form

DOI10.1016/0304-3975(89)90137-0MaRDI QIDQ1118577zbMATH OpenOpenAlexFDO

Authors Patrice Enjalbert, Luis Fariñas del Cerro

Publication date 1989

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

Full work available at URL https://doi.org/10.1016/0304-3975(89)90137-0

zbMATH Keywords

decision proceduresmultimodal logicsresolution systems for propositional modal logics

Mathematics Subject Classification ID

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

Recommendations

• Publication:4207883
• scientific article; zbMATH DE number 3932427
• Resolution-based methods for modal logics
• Clausal resolution for normal modal logics
• Decidability by resolution for propositional modal logics

Cites work

• scientific article; zbMATH DE number 4014675 (Why is no real title available?)
• scientific article; zbMATH DE number 3904560 (Why is no real title available?)
• scientific article; zbMATH DE number 4025402 (Why is no real title available?)
• scientific article; zbMATH DE number 3315203 (Why is no real title available?)
• scientific article; zbMATH DE number 3325547 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Modal Herbrand's Property
• A simple deduction method for modal logic
• MOLOG: A system that extends PROLOG with modal logic

Cited in

(27)

• Capturing equilibrium models in modal logic
• Multimodal logic programming using equational and order-sorted logic
• Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
• TABLEAUX: A general theorem prover for modal logics
• Proof complexity of modal resolution
• The recursive resolution method for modal logic
• 3-SAT = SAT for a class of normal modal logics
• A hybrid reasoning system for terminologies and first-order clauses in knowledge bases
• Clausal resolution for modal logics of confluence
• A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics
• scientific article; zbMATH DE number 3902618 (Why is no real title available?)
• Resolution calculi for non-normal modal logics
• A tableau-like proof procedure for normal modal logics
• The resolution method for one reducible class of formulas of the first-order modal logic S4.
• scientific article; zbMATH DE number 510785 (Why is no real title available?)
• Resolution with order and selection for hybrid logics
• scientific article; zbMATH DE number 4128785 (Why is no real title available?)
• Resolution for some first-order modal systems
• scientific article; zbMATH DE number 1735878 (Why is no real title available?)
• Linear strategy for propositional modal resolution
• Clausal resolution in a logic of rational agency
• Deciding the guarded fragments by resolution
• Temporal representation and reasoning in artificial intelligence: A review
• Rewrite rule systems for modal propositional logic
• scientific article; zbMATH DE number 4066840 (Why is no real title available?)
• The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics
• scientific article; zbMATH DE number 3932427 (Why is no real title available?)

This page was built for publication: Modal resolution in clausal form

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