Theorem proving using clausal resolution: from past to present

DOI10.1007/978-3-030-89716-1_2OpenAlexW3209686037MaRDI QIDQ2695485

Clare Dixon

Publication date: 31 March 2023

Full work available at URL: https://doi.org/10.1007/978-3-030-89716-1_2

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• VAMPIRE
• SPASS
• TeMP
• TRP++
• CTL-RP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using branching time temporal logic to synthesize synchronization skeletons
• The power of temporal proofs
• Temporal resolution using a breadth-first search algorithm
• Decidable fragments of first-order temporal logics
• Efficient local reductions to basic modal logic
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Mechanising first-order temporal resolution
• : A Resolution-Based Prover for Multimodal K
• An Introduction to Practical Formal Methods Using Temporal Logic
• Implementing a fair monodic temporal logic prover
• CTL-RP: A computation tree logic resolution prover
• System Description: Spass Version 3.0
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• A clausal resolution method for CTL branching-time temporal logic
• Search strategies for resolution in temporal logics
• Modal Resolution
• A Refined Resolution Calculus for CTL
• Monodic temporal resolution
• Automated Reasoning
• A resolution calculus for the branching-time temporal logic CTL
• Clausal resolution for normal modal logics
• Clausal temporal resolution

This page was built for publication: Theorem proving using clausal resolution: from past to present