Theorem proving using clausal resolution: from past to present
From MaRDI portal
Cites work
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
- A clausal resolution method for CTL branching-time temporal logic
- A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
- A Refined Resolution Calculus for CTL
- A resolution calculus for the branching-time temporal logic CTL
- An introduction to practical formal methods using temporal logic
- Automated Reasoning
- Clausal resolution for normal modal logics
- Clausal temporal resolution
- CTL-RP: A computation tree logic resolution prover
- Decidable fragments of first-order temporal logics
- Efficient local reductions to basic modal logic
- Handbook of modal logic
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 67448 (Why is no real title available?)
- scientific article; zbMATH DE number 1444729 (Why is no real title available?)
- Implementing a fair monodic temporal logic prover
- Mechanising first-order temporal resolution
- Modal Resolution
- Monodic temporal resolution
- Resolution theorem proving
- Search strategies for resolution in temporal logics
- System Description: Spass Version 3.0
- Temporal resolution using a breadth-first search algorithm
- The power of temporal proofs
- Using branching time temporal logic to synthesize synchronization skeletons
Cited in
(2)
This page was built for publication: Theorem proving using clausal resolution: from past to present
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2695485)
