SPASS

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

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

1 2 3 ... 8 9 10 next

  1. Bromberger, Martin; Dragoste, Irina; Faqeh, Rasha; Fetzer, Christof; Krötzsch, Markus; Weidenbach, Christoph: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (2021)
  2. Claessen, Koen; Lillieström, Ann: Handling transitive relations in first-order automated reasoning (2021)
  3. Duarte, André; Korovin, Konstantin: AC simplifications and closure redundancies in the superposition calculus (2021)
  4. Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
  5. Rosenberger, Tobias; Bensalem, Saddek; Knapp, Alexander; Roggenbach, Markus: Institution-based encoding and verification of simple UML state machines in CASL/SPASS (2021)
  6. Suda, Martin: Vampire with a brain is a good ITP hammer (2021)
  7. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  8. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  9. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  10. Cialdea Mayer, Marta: A prover dealing with nominals, binders, transitivity and relation hierarchies (2020)
  11. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
  12. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  13. Riesco, Adrián; Ogata, Kazuhiro: CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (2020)
  14. Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
  15. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  16. Bromberger, Martin; Fleury, Mathias; Schwarz, Simon; Weidenbach, Christoph: SPASS-SATT. A CDCL(LA) solver (2019)
  17. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  18. Davis, Ernest: Proof verification technology and elementary physics (2019)
  19. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
  20. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)

1 2 3 ... 8 9 10 next


Further publications can be found at: http://www.spass-prover.org/publications.html