SCOTT: Semantically Constrained Otter. The SCOTT project dates back to 1991 and is still running. The theorem prover, a variant of OTTER, has competed in CASC for several years, achieving unspectacular but interesting results. It is widely regarded as an idea that ought to work but has not yet realised its potential. The program is freely available. Like anything free, it comes with no guarantee. Unlike some free things, it also comes with no documentation: it remains very much work in progress and should be regarded as experimental software

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

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

1 2 next

  1. Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno: Scavenger 0.1: a theorem prover based on conflict resolution (2017)
  2. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  3. Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
  4. Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
  5. de Nivelle, Hans; Meng, Jia: Geometric resolution: a proof procedure based on finite model search (2006)
  6. Peltier, Nicolas: Model building with ordered resolution: Extracting models from saturated clause sets (2003)
  7. Choi, Seungyeob: Towards semantic goal-directed forward reasoning in resolution (2002)
  8. Choi, Seungyeob; Kerber, Manfred: Semantic selection for resolution in clause graphs (2002)
  9. Hodgson, Kahlil; Slaney, John: TPTP, CASC and the development of a semantically guided theorem prover (2002)
  10. Caferra, Ricardo; Peltier, Nicolas; Puitg, François: Emphasizing human techniques in automated geometry theorem proving: A practical realization (2001)
  11. Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.): Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings (2001)
  12. Hodgson, Kahlil; Slaney, John: System description: SCOTT-5 (2001)
  13. Koriche, Frédéric: A logic for approximate first-order reasoning (2001)
  14. Voronkov, Andrei: Algorithms, datastructures, and other issues in efficient automated deduction (2001)
  15. Brown, Marianne; Sutcliffe, Geoff: System description: PTTP + GLiDeS. Semantically guided PTTP (2000)
  16. Caferra, Ricardo; Peltier, Nicolas: Combining enumeration and deductive techniques in order to increase the class of constructible infinite models (2000)
  17. Dierkes, Michael: An application of model building in a resolution decision procedure for guarded formulas (2000)
  18. Stolzenburg, Frieder: Loop-detection in hyper-tableaux by powerful model generation (1999)
  19. Peltier, Nicolas: A new method for automated finite model building exploiting failures and symmetries (1998)
  20. Schaub, Torsten: The automation of reasoning with incomplete information. From semantic foundations to efficient computation (1998)

1 2 next