Removing irrelevant information in temporal resolution proofs

DOI10.1080/095281399146634zbMath1054.68639OpenAlexW2022782457MaRDI QIDQ4421286

Clare Dixon

Publication date: 1999

Published in: Journal of Experimental & Theoretical Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/095281399146634

zbMATH Keywords

temporal theorem proving

Mathematics Subject Classification ID

Uses Software

• OTTER
• SICStus
• STeP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Myths about the mutual exclusion problem
• Verifying concurrent processes using temporal logic
• Temporal resolution using a breadth-first search algorithm
• Nonclausal deduction in first-order temporal logic
• The complexity of propositional linear temporal logics
• Proving Liveness Properties of Concurrent Programs
• Resolution for temporal logics of knowledge
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle