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 84 articles )

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

1 2 3 4 5 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  3. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  4. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  5. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  6. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  7. 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)
  8. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  9. James, Phillip; Roggenbach, Markus: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (2014)
  10. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  11. Bridge, James P.; Paulson, Lawrence Charles: Case splitting in an automatic theorem prover for real-valued special functions (2013)
  12. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  13. Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
  14. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  15. Fietzke, Arnaud; Kruglov, Evgeny; Weidenbach, Christoph: Automatic generation of invariants for circular derivations in SUP(LA) (2012)
  16. Areces, Carlos; Gorín, Daniel: Unsorted functional translations (2011)
  17. Areces, Carlos; Gorín, Daniel: Resolution with order and selection for hybrid logics (2011)
  18. Baumgartner, Peter; Waldmann, Uwe: A combined superposition and model evolution calculus (2011)
  19. Burel, Guillaume: Experimenting with deduction modulo (2011)
  20. Claessen, Koen; Lillieström, Ann: Automated inference of finite unsatisfiability (2011)

1 2 3 4 5 next

Further publications can be found at: