Automating free logic in HOL, with an experimental application in category theory (Q2303232)

From MaRDI portal
Revision as of 21:47, 17 December 2024 by Import241208061232 (talk | contribs) (Normalize DOI.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
Automating free logic in HOL, with an experimental application in category theory
scientific article

    Statements

    title
    Automating free logic in HOL, with an experimental application in category theory (English)
    0 references
    author
    Christoph Benzmüller
    0 references
    Dana S. Scott
    0 references
    publication date
    3 March 2020
    0 references
    zbMATH Keywords
    free logic
    0 references
    classical higher-order logic
    0 references
    category theory
    0 references
    interactive and automated theorem proving
    0 references
    describes a project that uses
    Isabelle/HOL
    0 references
    E Theorem Prover
    0 references
    Nitpick
    0 references
    Archive Formal Proofs
    0 references
    LEO-II
    0 references
    SPASS
    0 references
    z3
    0 references
    HOL
    0 references
    VAMPIRE
    0 references
    Isabelle
    0 references
    TPTP
    0 references
    Satallax
    0 references
    Sledgehammer
    0 references
    CVC4
    0 references
    Leo-III
    0 references

    Identifiers

    Mathematics Subject Classification ID
    68V15
    0 references
    03B16
    0 references
    03B35
    0 references
    03B60
    0 references
    18A15
    0 references
    zbMATH DE Number
    7176592
    0 references
    OpenAlex ID
    W2908410917
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q2303232&oldid=38996846"
    Powered by MediaWiki