Hammer for Coq: automation for dependent type theory
From MaRDI portal
Publication:1663240
DOI10.1007/S10817-018-9458-4zbMATH Open1448.68458OpenAlexW2792493843WikidataQ90699792 ScholiaQ90699792MaRDI QIDQ1663240FDOQ1663240
Authors: Łukasz Czajka, Cezary Kaliszyk 
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
Recommendations
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- MizAR 40 for Mizar 40
- The TPTP World -- infrastructure for automated reasoning
- Mizar: State-of-the-art and Beyond
- A Brief Overview of HOL4
- Matita Tutorial
- Why3 — Where Programs Meet Provers
- MPTP-motivation, implementation, first experiments
- System Description: E 1.8
- The Lean Theorem Prover (System Description)
- Title not available (Why is that?)
- PRocH: Proof Reconstruction for HOL Light
- Idris, a general-purpose dependently typed programming language: Design and implementation
- SEPIA: Search for Proofs Using Inferred Automata
- 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
- 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
- Translating higher-order clauses to first-order clauses
- Semi-intelligible Isar proofs from machine-generated proofs
- Overview and evaluation of premise selection techniques for large theory mathematics
- An introduction to small scale reflection in Coq
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- HOL Light: An Overview
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- A Short Presentation of Coq
- Sine qua non for large theory reasoning
- Fast LCF-Style Proof Reconstruction for Z3
- One Logic to Use Them All
- The calculus of constructions
- On Long Normal Inhabitants of a Type
- A learning-based fact selector for Isabelle/HOL
- Intuitionistic games: determinacy, completeness, and normalization
- Title not available (Why is that?)
- A Brief Overview of Agda – A Functional Language with Dependent Types
- The Four Colour Theorem: Engineering of a Formal Proof
- A Machine-Checked Proof of the Odd Order Theorem
- Learning-assisted theorem proving with millions of lemmas
- Contraction-free sequent calculi for intuitionistic logic
- Mizar’s Soft Type System
- Random Forests for Premise Selection
- Hammering towards QED
- Automated proof construction in type theory using resolution
- A Complete Proof Synthesis Method for the Cube of Type Systems
- Types for Proofs and Programs
- Title not available (Why is that?)
- Automata theory approach to predicate intuitionistic logic
- Congruence Closure in Intensional Type Theory
- Smart matching
- Optimized encodings of fragments of type theory in first-order logic
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Frontiers of Combining Systems
Cited In (24)
- A monadic second-order version of Tarski's geometry of solids
- Relaxed weighted path order in theorem proving
- Restricted combinatory unification
- Superposition with lambdas
- Aligning concepts across proof assistant libraries
- Portfolio theorem proving and prover runtime prediction for geometry
- Title not available (Why is that?)
- Making higher-order superposition work
- Superposition with lambdas
- A combinator-based superposition calculus for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- CoqHammer
- An automatically verified prototype of the Android permissions system
- Making higher-order superposition work
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Extending SMT solvers to higher-order logic
- Experiences from exporting major proof assistant libraries
- Practical Proof Search for Coq by Type Inhabitation
- Formal Verification of Bit-Vector Invertibility Conditions in Coq
- Theorem proving as constraint solving with coherent logic
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Title not available (Why is that?)
- A Knuth-Bendix-like ordering for orienting combinator equations
Uses Software
This page was built for publication: Hammer for Coq: automation for dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663240)
