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

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

1 2 3 ... 6 7 8 next

  1. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  2. Klimek, Radosław: Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models (2019)
  3. Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
  4. Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
  5. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  6. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
  7. Echenim, Mnacho; Peltier, Nicolas; Sellami, Yanis: A generic framework for implicate generation modulo theories (2018)
  8. Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
  9. Nalon, Cláudia; Pattinson, Dirk: A resolution-based calculus for preferential logics (2018)
  10. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  11. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  12. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  13. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  14. Davis, Ernest; Marcus, Gary; Frazier-Logue, Noah: Commonsense reasoning about containers using radically incomplete information (2017)
  15. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  16. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  17. Cerna, David M.; Leitsch, Alexander: Schematic cut elimination and the ordered pigeonhole principle (2016)
  18. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2016)
  19. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  20. Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)

1 2 3 ... 6 7 8 next


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