Normal forms and proofs in combined modal and temporal logics

DOI10.1007/10720084_6MaRDI QIDQ4518865zbMATH OpenFDO

Authors Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher

Publication date 9 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

combined logicsdecision proceduremodal logicnormal formsresolutiontemporal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Review text

The paper presents a framework for automated theorem proving in multi-modal logics combined with LTL-based temporal dimension. It is a combination of a translation of the modal fragment into a first-order logic and then using first-order resolution and a direct, temporal resolution method for the temporal fragment which is transformed in a certain clausal form, using techniques and ideas from [\textit{C. Dixon, M. Fisher} and \textit{M. Wooldridge}, J. Log. Comput. 8, No. 3, 345-372 (1998; Zbl 0951.03007)] and a translation of de Nivelle substituting new variables for boxed subformulas. The resolution calculus introduced for that framework is shown to be sound, terminating and complete for combinations of particular subsystems of the multi-modal S5 (obtained by combining the axiom schemata 4, 5, B, D, T) with LTL, thus providing a decision procedure for such logics, although no complexity bounds for that procedure are provided. An extended version of that paper is available at \url{http://www.card.mmu.ac.uk/U.Hustadt/publications/HDSF2000b.ps.gz}. For the entire collection see [Zbl 0935.00044].

Recommendations

• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• scientific article; zbMATH DE number 475184
• Combined temporal and modal logic. Completeness results for predicate logic languages
• Normal form expressions of propositional projection temporal logic
• scientific article; zbMATH DE number 3966022
• Normal forms in combinatory logic
• scientific article; zbMATH DE number 6287570
• scientific article; zbMATH DE number 4053579
• Modal and temporal extensions of non-distributive propositional logics
• A functional approach for temporal \(\times\) modal logics

Cited in

(2)

• Clausal resolution in a logic of rational agency
• Alternating automata and temporal logic normal forms

This page was built for publication: Normal forms and proofs in combined modal and temporal logics

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