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

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

1 2 3 4 next

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

1 2 3 4 next