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
References in zbMATH (referenced in 71 articles , 1 standard article )
Showing results 1 to 20 of 71.
Sorted by year (- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Hillenbrand, Thomas; Weidenbach, Christoph: Superposition for bounded domains (2013)
- Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
- 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)
- 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)
- Kowalski, Robert; Sadri, Fariba: Abductive logic programming agents with destructive databases (2011)
- Baumgartner, Peter; Furbach, Ulrich; Pelzer, Björn: The hyper tableaux calculus with equality and an application to finite model computation (2010)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
- De Raedt, Luc: About knowledge and inference in logical and relational learning (2010)
- Constable, Robert; Moczydłowski, Wojciech: Extracting the resolution algorithm from a completeness proof for the propositional calculus (2009)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Baumgartner, Peter; Tinelli, Cesare: The model evolution calculus as a first-order DPLL method (2008)
- Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: $\alpha$\ssflean\itTAP: a declarative theorem prover for first-order classical logic (2008)
- Peltier, Nicolas: Automated model building: From finite to infinite models (2008)
- 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
- Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
- Pelzer, Björn; Wernhard, Christoph: System description: E-KRHyper (2007)
- Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2006)
- Eiter, Thomas; Gottlob, Georg: Reasoning under minimal upper bounds in propositional logic (2006)
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)