Mechanizing the metatheory of sledgehammer

Conference paper

Blanchette, J. and Popescu, A. 2013. Mechanizing the metatheory of sledgehammer. 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013). Nancy, France 18 - 20 Sep 2013 Springer. pp. 245-260
TypeConference paper
TitleMechanizing the metatheory of sledgehammer
AuthorsBlanchette, J. and Popescu, A.
Abstract

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.

Research GroupFoundations of Computing group
Conference9th International Symposium on Frontiers of Combining Systems (FroCoS 2013)
Page range245-260
ISSN0302-9743
ISBN
Hardcover9783642408847
PublisherSpringer
Publication dates
Print2013
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-40885-4_17

Additional information

Online ISBN:9783642408854.
Published paper appears in: Frontiers of Combining Systems, Volume 8152 of the series Lecture Notes in Computer Science pp 245-260, 2013

Web address (URL)http://dx.doi.org/10.1007/978-3-642-40885-4_17
LanguageEnglish
Book titleFrontiers of Combining Systems: 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/85203

Log in to edit

Download files

Accepted author manuscript
FROCOS2013.pdf

  • 16
    total views
  • 7
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as