An Isabelle/HOL Formalization of the SCL(FOL) Calculus (Q6492734): Difference between revisions

@@ Property / cites work @@
+Locales: a module system for mathematical theories
+Normal rank
@@ Property / cites work @@
+A verified SAT solver framework with learn, forget, restart, and incrementality
+Normal rank
@@ Property / cites work @@
+A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
+Normal rank
@@ Property / cites work @@
+Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
+Normal rank
@@ Property / cites work @@
+SCL clause learning from simple models
@@ Property / cites work: SCL clause learning from simple models / rank @@
+Normal rank
@@ Property / cites work @@
+SCL(EQ): SCL for first-order logic with equality
@@ Property / cites work: SCL(EQ): SCL for first-order logic with equality / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Bachmair and Ganzinger's ordered resolution prover
+Normal rank
@@ Property / cites work @@
+Formalizing Bachmair and Ganzinger's ordered resolution prover
+Normal rank
@@ Property / cites work @@
+A comprehensive framework for saturation theorem proving
+Normal rank