Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877): Difference between revisions

@@ Property / describes a project that uses @@
+SMTCoq
@@ Property / describes a project that uses: SMTCoq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-030-79876-5_26
+Normal rank
@@ Property / OpenAlex ID @@
+W3180619128
@@ Property / OpenAlex ID: W3180619128 / rank @@
+Normal rank
@@ Property / cites work @@
+Reliable reconstruction of fine-grained proofs in a proof assistant
+Normal rank
@@ Property / cites work @@
+An Isabelle/HOL Formalisation of Green’s Theorem
+Normal rank
@@ Property / cites work @@
+An Isabelle/HOL formalisation of Green's theorem
@@ Property / cites work: An Isabelle/HOL formalisation of Green's theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Scalable fine-grained proofs for formula processing
+Normal rank
@@ Property / cites work @@
+Congruence Closure with Free Variables
@@ Property / cites work: Congruence Closure with Free Variables / rank @@
+Normal rank
@@ Property / cites work @@
+Extending SMT solvers to higher-order logic
@@ Property / cites work: Extending SMT solvers to higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Semi-intelligible Isar proofs from machine-generated proofs
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+MaSh: Machine Learning for Sledgehammer
@@ Property / cites work: MaSh: Machine Learning for Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848688
@@ Property / cites work: Q2848688 / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Revisiting enumerative instantiation
@@ Property / cites work: Revisiting enumerative instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Bachmair and Ganzinger's ordered resolution prover
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+SMT proof checking using a logical framework
@@ Property / cites work: SMT proof checking using a logical framework / rank @@
+Normal rank