Mechanising first-order temporal resolution

DOI10.1016/j.ic.2004.10.005zbMath1086.03009OpenAlexW2143353707WikidataQ98283898 ScholiaQ98283898MaRDI QIDQ2486579

Yanyan Li

Publication date: 5 August 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2004.10.005

zbMATH Keywords

Temporal logicsClausal resolutionMonodic fragment

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (11)

First-order temporal verification in practice ⋮ Parameterized verification of leader/follower systems via first-order temporal logic ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Temporal abductive reasoning about biochemical reactions ⋮ Theorem proving using clausal resolution: from past to present ⋮ First-Order Resolution Methods for Modal Logics ⋮ Using temporal logics of knowledge for specification and verification -- a case study ⋮ Fair Derivations in Monodic Temporal Reasoning ⋮ Temporal Verification of Fault-Tolerant Protocols ⋮ Deductive verification of simple foraging robotic behaviours ⋮ Temporal Logics of Knowledge and their Applications in Security

Uses Software

• VAMPIRE
• SPIN
• TeMP

Cites Work

• Temporal semantics for concurrent METATEM
• Concerning the semantic consequence relation in first-order temporal logic
• Incompleteness of first-order temporal logic with until
• Temporal resolution using a breadth-first search algorithm
• Many-dimensional modal logics: theory and applications
• Decidable fragments of first-order temporal logics
• Temporalising tableaux
• Axiomatizing the monodic fragment of first-order temporal logic
• Equality and monodic first-order temporal logic
• Monodic packed fragment with equality is decidable
• Theorem proving with ordering and equality constrained clauses
• Decidable fragments of first-order modal logics
• Decision procedures for BDI logics
• Resolution for temporal logics of knowledge
• Decidability and incompleteness results for first-order temporal logics of linear time
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• Automated Reasoning
• Clausal temporal resolution
• Automated Deduction – CADE-19
• Abstract State Machines 2004. Advances in Theory and Practice
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Mechanising first-order temporal resolution