SPASS is an automated theorem prover for first-order logic with equality. So the input for the prover is a first-order formula in our syntax. Running SPASS on such a formula results in the final output SPASS beiseite: Proof found. if the formula is valid, SPASS beiseite: Completion found. if the formula is not valid and because validity in first-order logic is undecidable, SPASS may run forever without producing any final result.

References in zbMATH (referenced in 83 articles )

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

1 2 3 4 5 next

  1. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  3. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  4. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  5. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  6. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  7. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  8. Stojanović {\Dj}urđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
  9. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  10. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Automated verification of relational while-programs (2014)
  11. James, Phillip; Roggenbach, Markus: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (2014)
  12. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  13. Bridge, James P.; Paulson, Lawrence Charles: Case splitting in an automatic theorem prover for real-valued special functions (2013)
  14. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  15. Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
  16. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  17. Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph: More SPASS with Isabelle. Superposition with hard sorts and configurable simplification (2012)
  18. Fietzke, Arnaud; Kruglov, Evgeny; Weidenbach, Christoph: Automatic generation of invariants for circular derivations in SUP(LA) (2012)
  19. Areces, Carlos; Gorín, Daniel: Unsorted functional translations (2011)
  20. Areces, Carlos; Gorín, Daniel: Resolution with order and selection for hybrid logics (2011)

1 2 3 4 5 next

Further publications can be found at: