SPASS(NLA)

 

Subproject

H1/2

Categories

Core algorithms, Model checker / solver for hybrid systems, Theorem prover for hybrid systems

Overview

SPASS(NLA) is a theorem prover for the hierarchic combination of non-linear arithmetic including transcedential functions with full first-order logic. For the arithmetic reasoning we emply iSAT.

Publications

A. Eggers, E. Kruglov, S. Kupferschmid, K. Scheibler, T. Teige, and C. Weidenbach. Superposition modulo non-linear arithmetic. In 8th international Symposium on Frontiers of Combining Systems (FroCos 2011), Lecture Notes in Artificial Intelligence. Springer, 2011. To Appear.

Benchmarks

Download

---

Manual

---

Status

Proof of Concept