Mechanising first-order temporal resolution
From MaRDI portal
Publication:2486579
DOI10.1016/J.IC.2004.10.005zbMATH Open1086.03009OpenAlexW2143353707WikidataQ98283898 ScholiaQ98283898MaRDI QIDQ2486579FDOQ2486579
Authors: 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
Recommendations
Cites Work
- Title not available (Why is that?)
- Temporal resolution using a breadth-first search algorithm
- Many-dimensional modal logics: theory and applications
- Resolution theorem proving
- Temporal logic. Vol. 2. Mathematical foundations and computational aspects
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Clausal temporal resolution
- Resolution decision procedures
- Title not available (Why is that?)
- Concerning the semantic consequence relation in first-order temporal logic
- Incompleteness of first-order temporal logic with until
- Decidable fragments of first-order temporal logics
- Automated Reasoning
- Temporalising tableaux
- Theorem proving with ordering and equality constrained clauses
- Computing small clause normal forms
- Paramodulation-based theorem proving
- Decidable fragments of first-order modal logics
- Decision procedures for BDI logics
- 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
- Title not available (Why is that?)
- Axiomatizing the monodic fragment of first-order temporal logic
- Temporal semantics for concurrent METATEM
- Temporalizing description logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Equality and monodic first-order temporal logic
- Monodic packed fragment with equality is decidable
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Resolution for temporal logics of knowledge
- Title not available (Why is that?)
- Title not available (Why is that?)
- Abstract State Machines 2004. Advances in Theory and Practice
Cited In (15)
- Fair Derivations in Monodic Temporal Reasoning
- First-order temporal verification in practice
- Temporal Verification of Fault-Tolerant Protocols
- Automated Deduction – CADE-20
- First-Order Resolution Methods for Modal Logics
- Handling equality in monodic temporal resolution
- Monodic temporal resolution.
- Parameterized verification of leader/follower systems via first-order temporal logic
- Using temporal logics of knowledge for specification and verification -- a case study
- On temporal logics with data variable quantifications: decidability and complexity
- Deductive verification of simple foraging robotic behaviours
- Theorem proving using clausal resolution: from past to present
- Temporal abductive reasoning about biochemical reactions
- Temporal logics of knowledge and their applications in security
- Title not available (Why is that?)
Uses Software
This page was built for publication: Mechanising first-order temporal resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486579)