More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification

Jasmin Blanchette 1 Andrei Popescu 1 Daniel Wand 2 Christoph Weidenbach 2, 3
1 TUM - Technical University of Munich
2 MPII - Max-Planck-Institut für Informatik
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Type de document :
Communication dans un congrès
Lennart Beringer and Amy Felty. Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. Springer, 7406, pp.345-360, 2012, LNCS
Liste complète des métadonnées
https://hal.inria.fr/hal-00760392
Contributeur : Stephan Merz <>
Soumis le : lundi 3 décembre 2012 - 18:53:07
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Identifiants

  • HAL Id : hal-00760392, version 1

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Jasmin Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach. More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification. Lennart Beringer and Amy Felty. Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. Springer, 7406, pp.345-360, 2012, LNCS. 〈hal-00760392〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

275

Contact


archive-ouverte@inria.fr