Hammer for Coq: automation for dependent type theory
From MaRDI portal
(Redirected from Publication:1663240)
Recommendations
Cites work
- scientific article; zbMATH DE number 1629953 (Why is no real title available?)
- scientific article; zbMATH DE number 1042221 (Why is no real title available?)
- scientific article; zbMATH DE number 1765687 (Why is no real title available?)
- scientific article; zbMATH DE number 7015112 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A Brief Overview of HOL4
- A Complete Proof Synthesis Method for the Cube of Type Systems
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A Short Presentation of Coq
- A learning-based fact selector for Isabelle/HOL
- A machine-checked proof of the odd order theorem
- An introduction to small scale reflection in Coq
- Automata theory approach to predicate intuitionistic logic
- Automated proof construction in type theory using resolution
- Congruence closure in intensional type theory
- Contraction-free sequent calculi for intuitionistic logic
- Fast LCF-Style Proof Reconstruction for Z3
- Frontiers of Combining Systems
- HOL Light: An Overview
- HOL(y)Hammer: online ATP service for HOL Light
- Hammering towards QED
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Intuitionistic games: determinacy, completeness, and normalization
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Learning-assisted theorem proving with millions of lemmas
- Lightweight relevance filtering for machine-generated resolution problems
- MPTP-motivation, implementation, first experiments
- Matita Tutorial
- MizAR 40 for Mizar 40
- Mizar: state-of-the-art and beyond
- Mizar’s Soft Type System
- On Long Normal Inhabitants of a Type
- One logic to use them all
- Optimized encodings of fragments of type theory in first-order logic
- Overview and evaluation of premise selection techniques for large theory mathematics
- PRocH: proof reconstruction for HOL Light
- Premise selection for mathematics by corpus analysis and kernel methods
- Random forests for premise selection
- SEPIA: search for proofs using inferred automata
- Semi-intelligible Isar proofs from machine-generated proofs
- Sine qua non for large theory reasoning
- Smart matching
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- System description: E 1.8
- The Four Colour Theorem: Engineering of a Formal Proof
- The Lean theorem prover (system description)
- The TPTP World -- infrastructure for automated reasoning
- The calculus of constructions
- Translating higher-order clauses to first-order clauses
- Types for Proofs and Programs
- Why3 -- where programs meet provers
Cited in
(31)- Relaxed weighted path order in theorem proving
- Restricted combinatory unification
- A monadic second-order version of Tarski's geometry of solids
- Superposition with lambdas
- Aligning concepts across proof assistant libraries
- Portfolio theorem proving and prover runtime prediction for geometry
- scientific article; zbMATH DE number 7199590 (Why is no real title available?)
- A combinator-based superposition calculus for higher-order logic
- Making higher-order superposition work
- Superposition with lambdas
- An interactive SMT tactic in Coq using abductive reasoning
- scientific article; zbMATH DE number 7204433 (Why is no real title available?)
- CoqHammer
- Reconstruction of SMT proofs with Lambdapi
- scientific article; zbMATH DE number 7649963 (Why is no real title available?)
- A shallow embedding of pure type systems into first-order logic
- Hammering higher order set theory
- Duper: a proof-producing superposition theorem prover for dependent type theory
- An automatically verified prototype of the Android permissions system
- Making higher-order superposition work
- Concrete semantics with Coq and CoqHammer
- Interoperability of proof systems with SC-TPTP
- 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)
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- A Knuth-Bendix-like ordering for orienting combinator equations
Describes a project that uses
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)
