Search strategies for resolution in temporal logics

DOI10.1007/3-540-61511-3_121zbMath1412.68218OpenAlexW1537740740MaRDI QIDQ4647556

Clare Dixon

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_121

zbMATH Keywords

temporal logicdisjunctive normal formlinear temporal logictemporal resolutionstart node

Mathematics Subject Classification ID

Temporal logic (03B44)

Related Items (3)

Theorem proving using clausal resolution: from past to present ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Clausal resolution in a logic of rational agency

Cites Work

• Myths about the mutual exclusion problem
• Verifying concurrent processes using temporal logic
• Nonclausal deduction in first-order temporal logic
• Specifying Concurrent Program Modules
• The complexity of propositional linear temporal logics
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Search strategies for resolution in temporal logics