SPASS+T

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.


References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  2. Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe: Beagle -- a hierarchic superposition theorem prover (2015)
  3. Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei: Extensional crisis and proving identity (2014)
  4. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  5. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
  6. Baumgartner, Peter; Bax, Joshua: Proving infinite satisfiability (2013)
  7. Blanchette, Jasmin Christian; Paskevich, Andrei: TFF1: the TPTP typed first-order form with rank-1 polymorphism (2013)
  8. Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
  9. Echenim, Mnacho; Peltier, Nicolas: An instantiation scheme for satisfiability modulo theories (2012)
  10. Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
  11. Akbarpour, Behzad; Paulson, Lawrence Charles: MetiTarski: An automatic theorem prover for real-valued special functions (2010)
  12. Ge, Yeting; Barrett, Clark; Tinelli, Cesare: Solving quantified verification conditions using satisfiability modulo theories (2009)
  13. Akbarpour, Behzad; Paulson, Lawrence C.: MetiTarski: An automatic prover for the elementary functions (2008)
  14. Höfner, Peter: Automated reasoning for hybrid systems -- two case studies (2008)
  15. Akbarpour, Behzad; Paulson, Lawrence C.: Extending a resolution prover for inequalities on elementary functions (2007)
  16. Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin: Using first-order theorem provers in the Jahob data structure verification system (2007)
  17. Kuncak, Viktor; Rinard, Martin: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic (2007)
  18. Ludwig, Michel; Waldmann, Uwe: An extension of the Knuth-Bendix ordering with LPO-like properties (2007)