SATCHMO: a theorem prover implemented in Prolog. The SATCHMO Theorem Prover was one of the first systems which used model generation, i.e. a bottom-up proof procedure. The prover was given by a small Prolog-program, which implements a tableau proof procedure. One restriction is that it requires range restricted formulae.

References in zbMATH (referenced in 68 articles , 1 standard article )

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

1 2 3 4 next

  1. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  2. Balduccini, Marcello (ed.); Son, Tran Cao (ed.): Logic programming, knowledge representation, and nonmonotonic reasoning. Essays dedicated to Michael Gelfond on the occasion of his 65th birthday (2011)
  3. Brünnler, Kai (ed.); Metcalfe, George (ed.): Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4--8, 2011. Proceedings (2011)
  4. Kowalski, Robert; Sadri, Fariba: Abductive logic programming agents with destructive databases (2011)
  5. Baumgartner, Peter; Furbach, Ulrich; Pelzer, Björn: The hyper tableaux calculus with equality and an application to finite model computation (2010)
  6. Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010)
  7. De Raedt, Luc: About knowledge and inference in logical and relational learning (2010)
  8. Constable, Robert; Moczydłowski, Wojciech: Extracting the resolution algorithm from a completeness proof for the propositional calculus (2009)
  9. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  10. Baumgartner, Peter; Tinelli, Cesare: The model evolution calculus as a first-order DPLL method (2008)
  11. Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: $\alpha$\ssflean\itTAP: a declarative theorem prover for first-order classical logic (2008)
  12. Peltier, Nicolas: Automated model building: From finite to infinite models (2008)
  13. Chao, Yu-Yan; He, Li-Feng; Nakamura, Tsuyoshi; Shi, Zheng-Hao; Suzuki, Kenji; Itoh, Hidenori: An improvement of Herbrand’s theorem and its application to model generation theorem proving (2007)
  14. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
  15. Pelzer, Björn; Wernhard, Christoph: System description: E-KRHyper (2007)
  16. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2006)
  17. Eiter, Thomas; Gottlob, Georg: Reasoning under minimal upper bounds in propositional logic (2006)
  18. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
  19. Bezem, Marc; Coquand, Thierry: Automating coherent logic (2005)
  20. Hustadt, Ullrich; Motik, Boris; Sattler, Ulrike: A decomposition rule for decision procedures by resolution-based calculi (2005)

1 2 3 4 next