A Vernacular for Coherent Logic (Q5495937): Difference between revisions

@@ Property / describes a project that uses @@
+ArgoCLP
@@ Property / describes a project that uses: ArgoCLP / 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 @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OMDoc
@@ Property / describes a project that uses: OMDoc / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+miz3
@@ Property / describes a project that uses: miz3 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2128184640
@@ Property / OpenAlex ID: W2128184640 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.3391
@@ Property / arXiv ID: 1405.3391 / rank @@
+Normal rank
@@ Property / cites work @@
+A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i>
@@ Property / cites work: A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i> / rank @@
+Normal rank
@@ Property / cites work @@
+The challenge of computer mathematics
@@ Property / cites work: The challenge of computer mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Coherent Logic
@@ Property / cites work: Automating Coherent Logic / rank @@
+Normal rank
@@ Property / cites work @@
+On the mechanization of the proof of Hessenberg's theorem in coherent logic
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Proof and Disproof in Isabelle/HOL
@@ Property / cites work: Automatic Proof and Disproof in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Skolem Machines and Geometric Logic
@@ Property / cites work: Skolem Machines and Geometric Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / 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 @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Obvious inferences
@@ Property / cites work: Obvious inferences / rank @@
+Normal rank
@@ Property / cites work @@
+Q3678266
@@ Property / cites work: Q3678266 / rank @@
+Normal rank
@@ Property / cites work @@
+A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
+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 @@
+Tarski's System of Geometry
@@ Property / cites work: Tarski's System of Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5495937