Mechanising first-order temporal resolution
From MaRDI portal
Publication:2486579
Recommendations
Cites work
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 747023 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1249651 (Why is no real title available?)
- scientific article; zbMATH DE number 976360 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1931652 (Why is no real title available?)
- scientific article; zbMATH DE number 1882041 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 1444729 (Why is no real title available?)
- scientific article; zbMATH DE number 2243382 (Why is no real title available?)
- A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Abstract State Machines 2004. Advances in Theory and Practice
- Automated Reasoning
- Axiomatizing the monodic fragment of first-order temporal logic
- Clausal temporal resolution
- Computing small clause normal forms
- Concerning the semantic consequence relation in first-order temporal logic
- Decidability and incompleteness results for first-order temporal logics of linear time
- Decidable fragments of first-order modal logics
- Decidable fragments of first-order temporal logics
- Decision procedures for BDI logics
- Equality and monodic first-order temporal logic
- Incompleteness of first-order temporal logic with until
- Many-dimensional modal logics: theory and applications
- Monodic packed fragment with equality is decidable
- Paramodulation-based theorem proving
- Resolution decision procedures
- Resolution for temporal logics of knowledge
- Resolution theorem proving
- Temporal logic. Vol. 2. Mathematical foundations and computational aspects
- Temporal resolution using a breadth-first search algorithm
- Temporal semantics for concurrent METATEM
- Temporalising tableaux
- Temporalizing description logics
- Theorem proving with ordering and equality constrained clauses
Cited in
(16)- scientific article; zbMATH DE number 1882041 (Why is no real title available?)
- Fair Derivations in Monodic Temporal Reasoning
- First-order temporal verification in practice
- Temporal Verification of Fault-Tolerant Protocols
- Automated Deduction – CADE-20
- Handling equality in monodic temporal resolution
- Parameterized verification of leader/follower systems via first-order temporal logic
- Monodic temporal resolution.
- Using temporal logics of knowledge for specification and verification -- a case study
- On temporal logics with data variable quantifications: decidability and complexity
- Monodic temporal resolution
- First-order resolution methods for modal logics
- Deductive verification of simple foraging robotic behaviours
- Theorem proving using clausal resolution: from past to present
- Temporal logics of knowledge and their applications in security
- Temporal abductive reasoning about biochemical reactions
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)
