Resolution for some first-order modal systems

DOI10.1016/0304-3975(91)90181-ZMaRDI QIDQ1178699zbMATH OpenFDO

Authors Marta Cialdea Mayer

Publication date 26 June 1992

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

Full work available at URL https://doi.org/10.1016/0304-3975(91)90181-Z

zbMATH Keywords

resolution method

Mathematics Subject Classification ID

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

Review text

In the wake of growing interest among computer scientists in intensional logics one of the problem fields is to make such logics accessible for automated deduction methods. Building on earlier approaches toward the propositional case the author develops the resolution method for the first-order modal logics \(D\) (the ``denotic \(T\)), \(T\), and \(S4\) up to an outline of the completeness and soundness proof of that method.

Recommendations

• scientific article; zbMATH DE number 3932427
• First-order resolution methods for modal logics
• scientific article; zbMATH DE number 1763647
• Resolution-based methods for modal logics

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Modal Herbrand's Property
• A simple deduction method for modal logic
• DAL -- a logic for data analysis
• Formalization of Properties of Functional Programs
• 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 3131074 (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 4066840 (Why is no real title available?)
• scientific article; zbMATH DE number 43239 (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?)
• Modal resolution in clausal form
• MOLOG: A system that extends PROLOG with modal logic
• Synthesis of Communicating Processes from Temporal Logic Specifications

Cited in

(12)

• Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic
• The resolution method for one reducible class of formulas of the first-order modal logic S4.
• scientific article; zbMATH DE number 3932427 (Why is no real title available?)
• scientific article; zbMATH DE number 4055570 (Why is no real title available?)
• A note on resolutions mod i
• Herbrand style proof procedures for modal logic
• scientific article; zbMATH DE number 1763647 (Why is no real title available?)
• First-order resolution methods for modal logics
• Destructive Modal Resolution
• First-order intensional logic
• Resolution calculi for non-normal modal logics
• Strategies for modal resolution: Results and problems

This page was built for publication: Resolution for some first-order modal systems

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