Theorem proving using clausal resolution: from past to present (Q2695485): Difference between revisions

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