Modal resolution in clausal form

DOI10.1016/0304-3975(89)90137-0zbMath0669.03009OpenAlexW2017094488MaRDI QIDQ1118577

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)

Related Items

The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics, A tableau-like proof procedure for normal modal logics, Proof complexity of modal resolution, Linear strategy for propositional modal resolution, Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction), Resolution with order and selection for hybrid logics, Capturing equilibrium models in modal logic, Resolution for some first-order modal systems, TABLEAUX: A general theorem prover for modal logics, 3-SAT = SAT for a class of normal modal logics, Multimodal logic programming using equational and order-sorted logic, A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics, A hybrid reasoning system for terminologies and first-order clauses in knowledge bases, Temporal representation and reasoning in artificial intelligence: A review, Clausal resolution in a logic of rational agency, Deciding the guarded fragments by resolution

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A simple deduction method for modal logic
• MOLOG: A system that extends PROLOG with modal logic
• A Modal Herbrand's Property