Temporal resolution using a breadth-first search algorithm
From MaRDI portal
Publication:1383357
DOI10.1023/A:1018942108420zbMath0976.03010OpenAlexW1488387378MaRDI QIDQ1383357
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: Temporal resolution using a breadth-first search algorithm
