The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790)

From MaRDI portal
Revision as of 01:01, 12 July 2024 by ReferenceBot (talk | contribs) (‎Changed an Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
The reflective Milawa theorem prover is sound (down to the machine code that runs it)
scientific article

    Statements

    title
    The reflective Milawa theorem prover is sound (down to the machine code that runs it) (English)
    0 references
    author
    Jared Davis
    0 references
    Magnus O. Myreen
    0 references
    publication date
    26 May 2016
    0 references
    zbMATH Keywords
    soundness
    0 references
    theorem proving
    0 references
    proof assistant
    0 references
    machine code
    0 references
    describes a project that uses
    ACL2
    0 references
    Isabelle
    0 references
    HOL
    0 references
    CakeML
    0 references
    OpenTheory
    0 references
    Coq
    0 references
    Isabelle/HOL
    0 references
    z3
    0 references
    HOL Light
    0 references
    NQTHM
    0 references
    Ivy
    0 references
    Jitawa
    0 references
    DRAT-trim
    0 references
    cites work
    HOL Light: An Overview
    0 references
    Inprocessing Rules
    0 references
    Meta Reasoning in ACL2
    0 references
    Q5537599
    0 references
    Q4040283
    0 references
    CakeML
    0 references
    Q2723435
    0 references

    Identifiers

    zbMATH DE Number
    6585237
    0 references
    OpenAlex ID
    W1904308182
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q286790&oldid=36252048"
    Powered by MediaWiki