SCOTT
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
Keywords for this software
References in zbMATH (referenced in 21 articles )
Showing results 1 to 20 of 21.
Sorted by year (- Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
- de Nivelle, Hans; Meng, Jia: Geometric resolution: a proof procedure based on finite model search (2006)
- Peltier, Nicolas: Model building with ordered resolution: Extracting models from saturated clause sets (2003)
- Choi, Seungyeob: Towards semantic goal-directed forward reasoning in resolution (2002)
- Choi, Seungyeob; Kerber, Manfred: Semantic selection for resolution in clause graphs (2002)
- Hodgson, Kahlil; Slaney, John: TPTP, CASC and the development of a semantically guided theorem prover (2002)
- Caferra, Ricardo; Peltier, Nicolas; Puitg, François: Emphasizing human techniques in automated geometry theorem proving: A practical realization (2001)
- Hodgson, Kahlil; Slaney, John: System description: SCOTT-5 (2001)
- Koriche, Frédéric: A logic for approximate first-order reasoning (2001)
- Voronkov, Andrei: Algorithms, datastructures, and other issues in efficient automated deduction (2001)
- Brown, Marianne; Sutcliffe, Geoff: System description: PTTP + GLiDeS. Semantically guided PTTP (2000)
- Caferra, Ricardo; Peltier, Nicolas: Combining enumeration and deductive techniques in order to increase the class of constructible infinite models (2000)
- Dierkes, Michael: An application of model building in a resolution decision procedure for guarded formulas (2000)
- Stolzenburg, Frieder: Loop-detection in hyper-tableaux by powerful model generation (1999)
- Peltier, Nicolas: A new method for automated finite model building exploiting failures and symmetries (1998)
- Schaub, Torsten: The automation of reasoning with incomplete information. From semantic foundations to efficient computation (1998)
- Schaub, Torsten; Brüning, Stefan: Prolog technology for default reasoning: proof theory and compilation techniques (1998)
- Matzinger, Robert: Computational representations of Herbrand models using grammars (1997)
- Slaney, John; Surendonk, Timothy: Combining finite model generation with theorem proving. Problems and prospects (1996)
- Schaub, T.: A new methodology for query answering in default logics via structure-oriented theorem proving (1995)