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

Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph

doi:10.1007/978-3-642-32347-8_24

Item

ITEM ACTIONSEXPORT

DownloadE-Mail

Please note that a newer version of this item is available:
https://pure.mpg.de/pubman/item/item_1857501_6

DetailsSummary

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

Blanchette, J. C., Popescu, A., Wand, D., & Weidenbach, C. (2012). More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification. In L. Beringer, & A. Felty (Eds.), Interactive Theorem Proving (pp. 345-360). Berlin: Springer.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-B7E8-2 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-002C-AC8D-3

Genre: Conference Paper

Latex : More {SPASS} with {Isabelle} : Superposition with Hard Sorts and Configurable Simplification

Files

show Files

Locators

show

Creators

show

hide

Creators:
Blanchette, Jasmin Christian¹, Author
Popescu, Andrei¹, Author
Wand, Daniel², Author
Weidenbach, Christoph², Author

Affiliations:
1External Organizations, ou_persistent22
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545

Content

show

Details

show

hide

Language(s): eng - English

Dates: Date issued: 2012

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: -

Identifiers: DOI: 10.1007/978-3-642-32347-8_24
BibTex Citekey: Wand2012
Other: Local-ID: E8D9DE077D054C23C12579FB0041779E-Wand2012

Degree: -

Event

show

hide

Title: Third International Conference on Interactive Theorem Proving

Place of Event: Princeton, NJ

Start-/End Date: 2012-08-13 - 2012-08-15

Legal Case

show

Project information

show

Source 1

show

hide

Title: Interactive Theorem Proving

Subtitle : Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings

Abbreviation : ITP 2012

Source Genre: Proceedings

Creator(s):
Beringer, Lennart¹, Editor
Felty, Amy¹, Editor

Affiliations:
1 External Organizations, ou_persistent22

Publ. Info: Berlin : Springer

Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 345 - 360 Identifier: ISBN: 978-3-642-32346-1

Source 2

show

hide

Title: Lecture Notes in Computer Science

Abbreviation : LNCS

Source Genre: Series

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 7406 Sequence Number: - Start / End Page: - Identifier: -