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

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

1 2 3 ... 7 8 9 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  3. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  4. Cialdea Mayer, Marta: A prover dealing with nominals, binders, transitivity and relation hierarchies (2020)
  5. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
  6. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  7. Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
  8. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  9. Bromberger, Martin; Fleury, Mathias; Schwarz, Simon; Weidenbach, Christoph: SPASS-SATT. A CDCL(LA) solver (2019)
  10. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  11. Davis, Ernest: Proof verification technology and elementary physics (2019)
  12. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
  13. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  14. Klimek, Radosław: Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models (2019)
  15. Li, Di Long; Tiu, Alwen: Combining proverif and automated theorem provers for security protocol verification (2019)
  16. Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
  17. Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
  18. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  19. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: A deontic logic reasoning infrastructure (2018)
  20. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)

1 2 3 ... 7 8 9 next

Further publications can be found at: