Theorem proving using clausal resolution: from past to present
From MaRDI portal
Publication:2695485
DOI10.1007/978-3-030-89716-1_2OpenAlexW3209686037MaRDI QIDQ2695485
Publication date: 31 March 2023
Full work available at URL: https://doi.org/10.1007/978-3-030-89716-1_2
Uses Software
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