Resolution theorem proving in reified modal logics

DOI10.1007/BF00881845MaRDI QIDQ1332644zbMATH OpenFDO

Authors J. Stuart Aitken, Han Reichgelt, Nigel Shadbolt

Publication date 20 April 1995

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00881845

zbMATH Keywords

modal logic reified logics

Mathematics Subject Classification ID

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

Review text

Non-classical logical systems are usually defined axiomatically. Set of axioms together with inference rules and rules of necessitation define a particular logic. An alternative approach is to define the semantics of the modal or temporal logic in first-order logic. This is known as the reified approach. In the reified approach to defining logical systems the semantics of the reified logics are defined by axioms in first-order logics. The present paper presents new empirical and theoretical work on theorem proving in reified logics. The rewriting methods and world-path methods used are not new but have been used in a novel application. The advantage of the approach is that the reified logics are represented in a logical system whose semantics and proof methods are well understood. First-order logic provides a sound framework for proving theorems of a reified logic. One consequence of adopting the reified approach is that if we wish to automate proofs for modal systems, then any of the standard theorem- proving methods for first-order logic can be used to implement a theorem prover for a reified modal logic.

Recommendations

Cites work

Cited in

(10)

Describes a project that uses

Uses Software

TABLEAUX

This page was built for publication: Resolution theorem proving in reified modal logics

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