Extending Sledgehammer with SMT Solvers (Q5200019): Difference between revisions

From MaRDI portal
← Older edit
Added link to MaRDI item.
ReferenceBot (talk | contribs)
Bots
1,895,659 edits
‎Changed an Item
 
(24 intermediate revisions by 4 users not shown)
Property / author
 
Property / author: Lawrence Charles Paulson / rank
Normal rank
 
Property / author
 
Property / author: Lawrence Charles Paulson / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Archive Formal Proofs / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Coq / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Yices / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL Light / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Satallax / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL-Boogie / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: MPTP 0.2 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: z3 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: VAMPIRE / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ETPS / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: CVC Lite / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Robbins Conjecture / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Metis_ / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: cvc3 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: LEO-II / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: SMT-LIB / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: VCC / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Gandalf / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: SystemOnTPTP / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_11 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W1674186056 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4524769 / rank
 
Normal rank
Property / cites work
 
Property / cites work: An introduction to mathematical logic and type theory: To truth through proof. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Analytic Tableaux for Higher-Order Logic with Choice / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verification of clock synchronization algorithms: experiments on a combination of deductive tools / rank
 
Normal rank
Property / cites work
 
Property / cites work: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automated proof construction in type theory using resolution / rank
 
Normal rank
Property / cites work
 
Property / cites work: HOL-Boogie -- an interactive prover-backend for the verifying C compiler / rank
 
Normal rank
Property / cites work
 
Property / cites work: Sledgehammer: Judgement Day / rank
 
Normal rank
Property / cites work
 
Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Property-directed incremental invariant generation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Handling Polymorphism in Automated Deduction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Tools and Algorithms for the Construction and Analysis of Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Sine Qua Non for Large Theory Reasoning / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Polymorphic Intermediate Verification Language: Design and Logical Encoding / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2848688 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Translating higher-order clauses to first-order clauses / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lightweight relevance filtering for machine-generated resolution problems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2751358 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Source-Level Proof Reconstruction for Interactive Theorem Proving / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3150300 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automated Reasoning / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4664927 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2723436 / rank
 
Normal rank
Property / cites work
 
Property / cites work: MPTP 0.2: Design, implementation, and initial experiments / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2751379 / rank
 
Normal rank

Latest revision as of 09:09, 4 July 2024

scientific article; zbMATH DE number 5934346
Language Label Description Also known as
English
Extending Sledgehammer with SMT Solvers
scientific article; zbMATH DE number 5934346

    Statements

    title
    Extending Sledgehammer with SMT Solvers (English)
    0 references
    publication date
    29 July 2011
    0 references
    zbMATH DE Number
    5934346
    0 references
    Wikidata QID
    Q57382606
    0 references
    describes a project that uses
    Archive Formal Proofs
    0 references
    Coq
    0 references
    Yices
    0 references
    HOL Light
    0 references
    Satallax
    0 references
    HOL-Boogie
    0 references
    MPTP 0.2
    0 references
    z3
    0 references
    VAMPIRE
    0 references
    ETPS
    0 references
    CVC Lite
    0 references
    Robbins Conjecture
    0 references
    Metis_
    0 references
    cvc3
    0 references
    LEO-II
    0 references
    Isabelle/HOL
    0 references
    SMT-LIB
    0 references
    VCC
    0 references
    Gandalf
    0 references
    SystemOnTPTP
    0 references
    OpenAlex ID
    W1674186056
    0 references
    cites work
    Q4524769
    0 references
    Q2848688
    0 references
    Q2751358
    0 references
    Q3150300
    0 references
    Automated Reasoning
    0 references
    Q4664927
    0 references
    Q2723436
    0 references
    Q2751379
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q5200019&oldid=35240711"
    Powered by MediaWiki