Towards bit-width-independent proofs in SMT solvers (Q2305428): Difference between revisions

@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Q2703808
@@ Property / cites work: Q2703808 / rank @@
+Normal rank
@@ Property / cites work @@
+Complexity of fixed-size bit-vector logics
@@ Property / cites work: Complexity of fixed-size bit-vector logics / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view
@@ Property / cites work: Decision procedures. An algorithmic point of view / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Solving quantified bit-vectors using invertibility conditions
+Normal rank
@@ Property / cites work @@
+Q4823141
@@ Property / cites work: Q4823141 / rank @@
+Normal rank
@@ Property / cites work @@
+Syntax-guided rewrite rule enumeration for SMT solvers
+Normal rank
@@ Property / cites work @@
+Unification with abstraction and theory instantiation in saturation-based reasoning
+Normal rank
@@ Property / cites work @@
+Revisiting enumerative instantiation
@@ Property / cites work: Revisiting enumerative instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided quantifier instantiation for synthesis in SMT
+Normal rank
@@ Property / cites work @@
+Designing theory solvers with extensions
@@ Property / cites work: Designing theory solvers with extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Logics in Artificial Intelligence
@@ Property / cites work: Logics in Artificial Intelligence / rank @@
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank