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 143 articles , 1 standard article )

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

1 2 3 ... 6 7 8 next

  1. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  2. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  3. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  4. Davis, Ernest; Marcus, Gary; Frazier-Logue, Noah: Commonsense reasoning about containers using radically incomplete information (2017)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  7. Cerna, David M.; Leitsch, Alexander: Schematic cut elimination and the ordered pigeonhole principle (2016)
  8. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2016)
  9. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  10. Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
  11. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  12. Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
  13. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  14. Chaudhari, Dipak L.; Damani, Om: Combining top-down and bottom-up techniques in program derivation (2015)
  15. Hustadt, Ullrich; Gainer, Paul; Dixon, Clare; Nalon, Cláudia; Zhang, Lan: Ordered resolution for coalition logic (2015)
  16. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  17. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  18. Stojanović Đurđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
  19. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  20. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Automated verification of relational while-programs (2014)

1 2 3 ... 6 7 8 next

Further publications can be found at: