Resolution with order and selection for hybrid logics
From MaRDI portal
Publication:2429982
In the paper the labeled resolution calculus for hybrid logics is presented. The authors show that the general framework of saturation-based reasoning for first-order logic with equality can be adapted to calculi for other logics. They show then that the calculus presented is complete for any admissible order and selection function. It gives a decision method for some fragment of hybrid logic. Since hybrid logics are extensions of modal logics, the results of the paper can also be applied to a number of modal logics.
Recommendations
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A Modal Herbrand's Property
- A new methodology for developing deduction methods
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- A simple deduction method for modal logic
- Clausal resolution for normal modal logics
- Decidability by resolution for propositional modal logics
- Deciding the guarded fragments by resolution
- Destructive Modal Resolution
- Handbook of automated reasoning. In 2 vols
- Handbook of modal logic
- scientific article; zbMATH DE number 4018413 (Why is no real title available?)
- scientific article; zbMATH DE number 3932427 (Why is no real title available?)
- scientific article; zbMATH DE number 4055570 (Why is no real title available?)
- scientific article; zbMATH DE number 15881 (Why is no real title available?)
- scientific article; zbMATH DE number 1215470 (Why is no real title available?)
- scientific article; zbMATH DE number 1341475 (Why is no real title available?)
- scientific article; zbMATH DE number 1059246 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 1765659 (Why is no real title available?)
- scientific article; zbMATH DE number 1765682 (Why is no real title available?)
- scientific article; zbMATH DE number 1860675 (Why is no real title available?)
- scientific article; zbMATH DE number 1424043 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3300566 (Why is no real title available?)
- scientific article; zbMATH DE number 3032487 (Why is no real title available?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Modal logic
- Modal resolution in clausal form
- MOLOG: A system that extends PROLOG with modal logic
- On the Restraining Power of Guards
- Paramodulation-based theorem proving
- Representation, reasoning, and relational structures: a hybrid logic manifesto
- Resolution calculi for modal logics
- Resolution in modal, description and hybrid logic
- Resolution theorem proving
- Resolution-based methods for modal logics
- Strategies for modal resolution: Results and problems
- Term Rewriting and All That
- The computational complexity of hybrid temporal logics
- Theory and Applications of Relational Structures as Knowledge Instruments
- Using resolution for testing modal satisfiability and building models
Cited in
(9)- Combining preorder and postorder resolution in a satisfiability solver
- Resolution in modal, description and hybrid logic
- Ordered resolution for coalition logic
- A Modal-Layered Resolution Calculus for K
- scientific article; zbMATH DE number 1761419 (Why is no real title available?)
- Modal Hybrid Logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- A hybrid calculus for logic \(N^{*}\): residual finiteness and decidability
- Proof complexity of modal resolution
This page was built for publication: Resolution with order and selection for hybrid logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2429982)
