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

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

1 2 3 ... 6 7 8 next

  1. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  2. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
  3. Echenim, Mnacho; Peltier, Nicolas; Sellami, Yanis: A generic framework for implicate generation modulo theories (2018)
  4. Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
  5. Nalon, Cláudia; Pattinson, Dirk: A resolution-based calculus for preferential logics (2018)
  6. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  7. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  8. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  9. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  10. Davis, Ernest; Marcus, Gary; Frazier-Logue, Noah: Commonsense reasoning about containers using radically incomplete information (2017)
  11. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  12. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  13. Cerna, David M.; Leitsch, Alexander: Schematic cut elimination and the ordered pigeonhole principle (2016)
  14. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2016)
  15. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  16. Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
  17. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover \textscLeo-II (2015)
  18. Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
  19. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  20. Chaudhari, Dipak L.; Damani, Om: Combining top-down and bottom-up techniques in program derivation (2015)

1 2 3 ... 6 7 8 next


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