Practical Proof Search for Coq by Type Inhabitation

DOI10.1007/978-3-030-51054-1_3OpenAlexW3039875133MaRDI QIDQ5048991

Łukasz Czajka

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_3

zbMATH Keywords

intuitionistic logicproof searchCoqproof automationinhabitationdependent type theory

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Theorem proving as constraint solving with coherent logic

Uses Software

• Coq
• ILTP
• Isabelle/HOL
• Satallax
• Automath
• CompCert
• leanCoP
• ileanCoP
• JProver
• Leo-III
• GitHub
• CoqHammer
• SMTCoq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The ILTP problem library for intuitionistic logic
• Lectures on the Curry-Howard isomorphism
• Isabelle/HOL. A proof assistant for higher-order logic
• Hammer for Coq: automation for dependent type theory
• The higher-order prover Leo-III
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Satallax: An Automatic Higher-Order Prover
• A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Contraction-free sequent calculi for intuitionistic logic
• A Complete Proof Synthesis Method for the Cube of Type Systems
• CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION
• Term Rewriting and All That
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• Hammering towards QED
• Types for Proofs and Programs
• On the Mints Hierarchy in First-Order Intuitionistic Logic
• Types for Proofs and Programs