Mechanizing the Metatheory of Sledgehammer

DOI10.1007/978-3-642-40885-4_17zbMATH Open1398.68479OpenAlexW2114237827MaRDI QIDQ2849493

Andrei Popescu, Jasmin Christian Blanchette

Publication date: 20 September 2013

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/15370/1/FROCOS2013.pdf

Mathematics Subject Classification ID

Related Items (10)

Lax Theory Morphisms ⋮ Soundness and completeness proofs by coinductive methods ⋮ Mechanizing metatheory in a logical framework ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Mechanizing the metatheory of LF ⋮ A formalized general theory of syntax with bindings ⋮ Encoding Monomorphic and Polymorphic Types ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Uses Software

• HOL
• Sledgehammer
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: Mechanizing the Metatheory of Sledgehammer

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2849493)