SATCHMO

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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