More SPASS with Isabelle: superposition with hard sorts and configurable simplification

Conference paper

Blanchette, J., Popescu, A., Wand, D. and Weidenbach, C. 2012. More SPASS with Isabelle: superposition with hard sorts and configurable simplification. Interactive Theorem Proving (ITP), Third International Conference. Princeton, New Jersey, US 13 - 15 Aug 2012 Springer. pp. 345-360
TypeConference paper
TitleMore SPASS with Isabelle: superposition with hard sorts and configurable simplification
AuthorsBlanchette, J., Popescu, A., Wand, D. and Weidenbach, C.
Abstract

Sledgehammer for Isabelle/HOL integrates automatic theorem provers to discharge interactive proof obligations. This paper considers a tighter integration of the superposition prover SPASS to increase Sledgehammer’s success rate. The main enhancements are native support for hard sorts (simple types) in SPASS, simplification that honors the orientation of Isabelle simp rules, and a pair of clause-selection strategies targeted at large lemma libraries. The usefulness of this integration is confirmed by an evaluation on a vast benchmark suite and by a
case study featuring a formalization of language-based security.

Research GroupFoundations of Computing group
ConferenceInteractive Theorem Proving (ITP), Third International Conference
Page range345-360
ISSN0302-9743
ISBN
Hardcover9783642323461
PublisherSpringer
Publication dates
Print2012
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-32347-8_24

Additional information

Online ISBN:9783642323478
Published paper appears in: Interactive Theorem Proving, Volume 7406 of the series Lecture Notes in Computer Science pp 345-360, 2012

Web address (URL)http://dx.doi.org/10.1007/978-3-642-32347-8_24
LanguageEnglish
Book titleInteractive Theorem Proving: third international conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/8520x

Log in to edit

Download files

Accepted author manuscript
ITP2012.pdf

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

Export as