Practical Proof Search for Coq by Type Inhabitation (Q5048991): Difference between revisions

@@ Property / describes a project that uses @@
+leanCoP
@@ Property / describes a project that uses: leanCoP / 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 @@
+Satallax
@@ Property / describes a project that uses: Satallax / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+JProver
@@ Property / describes a project that uses: JProver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMTCoq
@@ Property / describes a project that uses: SMTCoq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ILTP
@@ Property / describes a project that uses: ILTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Leo-III
@@ Property / describes a project that uses: Leo-III / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CompCert
@@ Property / describes a project that uses: CompCert / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoqHammer
@@ Property / describes a project that uses: CoqHammer / 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-51054-1_3
+Normal rank
@@ Property / OpenAlex ID @@
+W3039875133
@@ Property / OpenAlex ID: W3039875133 / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692618
@@ Property / cites work: Q4692618 / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / 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 @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+A Complete Proof Synthesis Method for the Cube of Type Systems
+Normal rank
@@ Property / cites work @@
+Contraction-free sequent calculi for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION
+Normal rank
@@ Property / cites work @@
+Admissibility of structural rules for contraction-free systems of intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Q3092752
@@ Property / cites work: Q3092752 / rank @@
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
+Normal rank
@@ Property / cites work @@
+Q4346206
@@ Property / cites work: Q4346206 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4520768
@@ Property / cites work: Q4520768 / rank @@
+Normal rank
@@ Property / cites work @@
+A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
+Normal rank
@@ Property / cites work @@
+Q4281483
@@ Property / cites work: Q4281483 / rank @@
+Normal rank
@@ Property / cites work @@
+The ILTP problem library for intuitionistic logic
@@ Property / cites work: The ILTP problem library for intuitionistic logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539627
@@ Property / cites work: Q4539627 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Mints Hierarchy in First-Order Intuitionistic Logic
+Normal rank
@@ Property / cites work @@
+Lectures on the Curry-Howard isomorphism
@@ Property / cites work: Lectures on the Curry-Howard isomorphism / rank @@
+Normal rank
@@ Property / cites work @@
+The higher-order prover Leo-III
@@ Property / cites work: The higher-order prover Leo-III / rank @@
+Normal rank
@@ Property / cites work @@
+Q4716271
@@ Property / cites work: Q4716271 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024919
@@ Property / cites work: Q3024919 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5771193
@@ Property / cites work: Q5771193 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999539
@@ Property / cites work: Q3999539 / rank @@
+Normal rank