Temporal resolution using a breadth-first search algorithm

DOI10.1023/A:1018942108420zbMath0976.03010OpenAlexW1488387378MaRDI QIDQ1383357

Clare Dixon

Publication date: 10 September 2000

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1018942108420

Mathematics Subject Classification ID

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

Related Items (11)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ Theorem proving using clausal resolution: from past to present ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Mechanising first-order temporal resolution ⋮ A Refined Resolution Calculus for CTL ⋮ Removing irrelevant information in temporal resolution proofs ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Clausal resolution in a logic of rational agency

Uses Software

• OTTER
• SICStus

This page was built for publication: Temporal resolution using a breadth-first search algorithm