First-order temporal verification in practice

DOI10.1007/s10817-005-7354-1zbMath1108.03018DBLPjournals/jar/Fernandez-GagoHDFK05OpenAlexW2065380071WikidataQ98283887 ScholiaQ98283887MaRDI QIDQ851137

N. E. Zubov

Publication date: 17 November 2006

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

Full work available at URL: https://doi.org/10.1007/s10817-005-7354-1

zbMATH Keywords

theorem provingresolutionfirst-order temporal logictemporal logics of knowledge

Mathematics Subject Classification ID

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

Related Items (3)

Parameterized verification of leader/follower systems via first-order temporal logic ⋮ Using temporal logics of knowledge for specification and verification -- a case study ⋮ Temporal Logics of Knowledge and their Applications in Security

Uses Software

• VAMPIRE
• TeMP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A structure-preserving clause form translation
• The complexity of reasoning about knowledge and time. I: Lower bounds
• Many-dimensional modal logics: theory and applications
• Decidable fragments of first-order temporal logics
• A survey of temporal extensions of description logics
• Monodic packed fragment with equality is decidable
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• On the feasibility of checking temporal integrity constraints
• Mechanising first-order temporal resolution
• Using encryption for authentication in large networks of computers
• Resolution for temporal logics of knowledge
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• On the Restraining Power of Guards
• Automated Reasoning
• Automated Deduction – CADE-19
• Automated Deduction – CADE-19

This page was built for publication: First-order temporal verification in practice