Practical Proof Search for Coq by Type Inhabitation
From MaRDI portal
Publication:5048991
DOI10.1007/978-3-030-51054-1_3OpenAlexW3039875133MaRDI QIDQ5048991
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
Related Items
Uses Software
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
