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

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

1 2 3 4 5 next

  1. Wernhard, Christoph: Craig interpolation with clausal first-order tableaux (2021)
  2. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  3. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  4. Kowalski, Robert; Sadri, Fariba: Programming in logic without logic programming (2016)
  5. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  6. Hillenbrand, Thomas; Weidenbach, Christoph: Superposition for bounded domains (2013)
  7. Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
  8. 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)
  9. 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)
  10. Kowalski, Robert; Sadri, Fariba: Abductive logic programming agents with destructive databases (2011)
  11. Baumgartner, Peter; Furbach, Ulrich; Pelzer, Björn: The hyper tableaux calculus with equality and an application to finite model computation (2010)
  12. Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
  13. De Raedt, Luc: About knowledge and inference in logical and relational learning (2010)
  14. Constable, Robert; Moczydłowski, Wojciech: Extracting the resolution algorithm from a completeness proof for the propositional calculus (2009)
  15. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  16. Baumgartner, Peter; Tinelli, Cesare: The model evolution calculus as a first-order DPLL method (2008)
  17. Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: (\alpha)\textsflean\textitTAP: a declarative theorem prover for first-order classical logic (2008)
  18. Peltier, Nicolas: Automated model building: From finite to infinite models (2008)
  19. 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) ioport
  20. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)

1 2 3 4 5 next