Mechanizing the metatheory of sledgehammer

Blanchette, Jasmin Christian; Popescu, Andrei (2013)
Springer
English
Array
This paper presents an Isabelle/HOL formalization of recent research in automated reasoning: efficient encodings of sorts in unsorted first-order logic, as implemented in Isabelle’s Sledgehammer proof tool. The formalization provides the general-purpose machinery to reason about formulas and models, emulating the theory of institutions. Quantifiers are represented using a nominal-like approach designed for interpreting syntax in semantic domains.

Download from

Cite this article

BibTeX

Chicago

IEEE