SPASS(LA)
Subproject |
H1/2, S2 |
Categories |
Core algorithms, Model checker / solver for hybrid systems, Theorem prover for hybrid systems |
Overview |
SPASS(LA) is a theorem prover for the hierarchic combination of linear arithmetic with full first-order logic. For the linear arithmetic reasoning we emply LP-solver as well as decision procedures for FOL(LA). |
E. Althaus, E. Kruglov, and C. Weidenbach. Superposition modulo linear arithmetic (la). In Silvio Ghilardi and Roberto Sebastiani, editors, 7th international Symposium on Frontiers of Combining Systems (FroCos 2009), volume 5749 of Lecture Notes in Artificial Intelligence, pages 84-99, 2009. |
|
Benchmarks |
|
Download |
--- |
Manual |
--- |
Status |
Proof of Concept |