SPASS+T

Virgile Prevosto and Uwe Waldmann

In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, ESCoR: Empirically Successful Computerized Reasoning, pages 18-33, Seattle, WA, USA, August 21, 2006, CEUR Workshop Proceedings, Vol. 192. [PDF file, 142 kB]

Abstract: SPASS+T is an extension of the superposition-based theorem prover SPASS that allows us to enlarge the reasoning capabilities of SPASS using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of SPASS+T and the capabilities, limitations, and applications of such a combination.

Download SPASS+T.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 2006-04-03.