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.
| Original language | English |
|---|---|
| Pages (from-to) | 18-33 |
| Number of pages | 16 |
| Journal | CEUR Workshop Proceedings |
| Volume | 192 |
| Publication status | Published - 1 Dec 2006 |
| Externally published | Yes |
| Event | FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, ESCoR 2006 - Seattle, WA, United States Duration: 22 Aug 2006 → 22 Aug 2006 |