Hammer for Coq: automation for dependent type theory
From MaRDI portal
Publication:1663240
DOI10.1007/s10817-018-9458-4zbMath1448.68458OpenAlexW2792493843WikidataQ90699792 ScholiaQ90699792MaRDI QIDQ1663240
Cezary Kaliszyk, Łukasz Czajka
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9458-4
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (21)
Practical Proof Search for Coq by Type Inhabitation ⋮ ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Aligning concepts across proof assistant libraries ⋮ An automatically verified prototype of the Android permissions system ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Relaxed weighted path order in theorem proving ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ CoqHammer ⋮ Experiences from exporting major proof assistant libraries ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Theorem proving as constraint solving with coherent logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MizAR 40 for Mizar 40
- Semi-intelligible Isar proofs from machine-generated proofs
- A learning-based fact selector for Isabelle/HOL
- Intuitionistic games: determinacy, completeness, and normalization
- Learning-assisted theorem proving with millions of lemmas
- MPTP-motivation, implementation, first experiments
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Lightweight relevance filtering for machine-generated resolution problems
- The calculus of constructions
- Automated proof construction in type theory using resolution
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Automata theory approach to predicate intuitionistic logic
- Translating higher-order clauses to first-order clauses
- Congruence Closure in Intensional Type Theory
- System Description: E 1.8
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- Random Forests for Premise Selection
- On Long Normal Inhabitants of a Type
- The TPTP World – Infrastructure for Automated Reasoning
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- HOL Light: An Overview
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Mizar: State-of-the-art and Beyond
- SEPIA: Search for Proofs Using Inferred Automata
- The Lean Theorem Prover (System Description)
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Mizar’s Soft Type System
- A Short Presentation of Coq
- A Brief Overview of HOL4
- Smart Matching
- The Four Colour Theorem: Engineering of a Formal Proof
- Contraction-free sequent calculi for intuitionistic logic
- Optimized encodings of fragments of type theory in first-order logic
- A Complete Proof Synthesis Method for the Cube of Type Systems
- One Logic to Use Them All
- PRocH: Proof Reconstruction for HOL Light
- Matita Tutorial
- Hammering towards QED
- Sine Qua Non for Large Theory Reasoning
- Why3 — Where Programs Meet Provers
- A Machine-Checked Proof of the Odd Order Theorem
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Frontiers of Combining Systems
- Types for Proofs and Programs
- Fast LCF-Style Proof Reconstruction for Z3
This page was built for publication: Hammer for Coq: automation for dependent type theory
