Semi-intelligible Isar proofs from machine-generated proofs (Q287340): Difference between revisions

@@ Property / describes a project that uses @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Satallax
@@ Property / describes a project that uses: Satallax / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CLSAT
@@ Property / describes a project that uses: CLSAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TRAMP
@@ Property / describes a project that uses: TRAMP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Robbins Conjecture
@@ Property / describes a project that uses: Robbins Conjecture / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Metis_
@@ Property / describes a project that uses: Metis_ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+veriT
@@ Property / describes a project that uses: veriT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaSh
@@ Property / describes a project that uses: MaSh / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PRocH
@@ Property / describes a project that uses: PRocH / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Waldmeister
@@ Property / describes a project that uses: Waldmeister / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Regular_Algebras
@@ Property / describes a project that uses: Regular_Algebras / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEO-II
@@ Property / describes a project that uses: LEO-II / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SystemOnTPTP
@@ Property / describes a project that uses: SystemOnTPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Network Security Policy Verification
+Normal rank
@@ Property / describes a project that uses @@
+Sqrt_Babylonian
@@ Property / describes a project that uses: Sqrt_Babylonian / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1216298300
@@ Property / OpenAlex ID: W1216298300 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113901251
@@ Property / Wikidata QID: Q113901251 / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Q2847390
@@ Property / cites work: Q2847390 / rank @@
+Normal rank
@@ Property / cites work @@
+Computing Tiny Clause Normal Forms
@@ Property / cites work: Computing Tiny Clause Normal Forms / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+Property-directed incremental invariant generation
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Encoding Monomorphic and Polymorphic Types
@@ Property / cites work: Encoding Monomorphic and Polymorphic Types / rank @@
+Normal rank
@@ Property / cites work @@
+More SPASS with Isabelle
@@ Property / cites work: More SPASS with Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
+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 @@
+Satallax: An Automatic Higher-Order Prover
@@ Property / cites work: Satallax: An Automatic Higher-Order Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4520767
@@ Property / cites work: Q4520767 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
+Normal rank
@@ Property / cites work @@
+Automated Analysis of Regular Algebra
@@ Property / cites work: Automated Analysis of Regular Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Untersuchungen über das logische Schliessen. I
@@ Property / cites work: Untersuchungen über das logische Schliessen. I / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+On the rules of suppositions in formal logic
@@ Property / cites work: On the rules of suppositions in formal logic / rank @@
+Normal rank
@@ Property / cites work @@
+PRocH: Proof Reconstruction for HOL Light
@@ Property / cites work: PRocH: Proof Reconstruction for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+Reducibility among Combinatorial Problems
@@ Property / cites work: Reducibility among Combinatorial Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997716
@@ Property / cites work: Q3997716 / 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 @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723444
@@ Property / cites work: Q2723444 / rank @@
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Equational reasoning in Isabelle
@@ Property / cites work: Equational reasoning in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Methods of lemma extraction in natural deduction proofs
+Normal rank
@@ Property / cites work @@
+Improving legibility of natural deduction proofs is not trivial
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Source-Level Proof Reconstruction for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q3338233
@@ Property / cites work: Q3338233 / rank @@
+Normal rank
@@ Property / cites work @@
+Obvious inferences
@@ Property / cites work: Obvious inferences / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / 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
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+Q2723436
@@ Property / cites work: Q2723436 / rank @@
+Normal rank
@@ Property / cites work @@
+Ribbon Proofs for Separation Logic
@@ Property / cites work: Ribbon Proofs for Separation Logic / rank @@
+Normal rank