Hammer for Coq: automation for dependent type theory (Q1663240)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Hammer for Coq: automation for dependent type theory
scientific article

    Statements

    title
    Hammer for Coq: automation for dependent type theory (English)
    0 references
    author
    Łukasz Czajka
    0 references
    Cezary Kaliszyk
    0 references
    publication date
    21 August 2018
    0 references
    zbMATH DE Number
    6921420
    0 references
    zbMATH Keywords
    hammer
    0 references
    Coq
    0 references
    calculus of inductive constructions
    0 references
    proof automation
    0 references
    describes a project that uses
    Isabelle
    0 references
    TPTP
    0 references
    Mizar
    0 references
    WEKA
    0 references
    JProver
    0 references
    HOLyHammer
    0 references
    Why3
    0 references
    Easychair
    0 references
    Idris
    0 references
    SEPIA
    0 references
    DeepMath
    0 references
    WhyML
    0 references
    ACL2
    0 references
    Coq
    0 references
    Metis_
    0 references
    Proof General
    0 references
    Agda
    0 references
    PRocH
    0 references
    E Theorem Prover
    0 references
    Lean
    0 references
    VAMPIRE
    0 references
    z3
    0 references
    HOL
    0 references
    HOL Light
    0 references
    ML4PG
    0 references
    Coq/SSReflect
    0 references
    Irdis
    0 references
    Flyspeck
    0 references
    OpenAlex ID
    W2792493843
    0 references
    Wikidata QID
    Q90699792
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q1663240&oldid=33217764"
    Powered by MediaWiki