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. |
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 |