FINDER
Finite domain enumerator. This is a finite domain CSP solver, rather limited in what it can do. Don’t expect it to deal effectively with anything numerical, though it can knock off small problems reasonably quickly. The nice feature (say I) is the input language which is first order logic thinly disguised. Earlier versions of this came with some documentation. This one comes with the injunction to use the Force (read the source). Also read the README that comes with it.
Keywords for this software
References in zbMATH (referenced in 37 articles )
Showing results 1 to 20 of 37.
Sorted by year (- Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
- Gajdoš, Petr; Kuřil, Martin: Ordered semigroups of size at most 7 and linearly ordered semigroups of size at most 10. (2014)
- Shah, Muhammad; Gretton, Charles; Sorge, Volker: Enumerating AG-groups with a study of Smaradache AG-groups. (2011)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
- Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
- Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare: Computing finite models by reduction to function-free clause logic (2009)
- Peltier, Nicolas: Constructing infinite models represented by tree automata (2009)
- Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)
- Peltier, Nicolas: Automated model building: From finite to infinite models (2008)
- Audemard, Gilles; Benhamou, Belaïd; Henocque, Laurent: Predicting and detecting symmetries in FOL finite model search (2006)
- Huang, Zhuo; Zhang, Jian: Generating SAT instances from first-order formulas (2005)
- Konrad, Karsten: Model generation for natural language interpretation and analysis. (2004)
- Zhang, Jian; Zhang, Hantao: Extending finite model searching with congruence closure computation (2004)
- Peltier, Nicolas: Extracting models from clause sets saturated under semantic refinements of the resolution rule. (2003)
- Peltier, Nicolas: A calculus combining resolution and enumeration for building finite models (2003)
- Choi, Seungyeob: Towards semantic goal-directed forward reasoning in resolution (2002)
- Dubois, Olivier; Dequen, Gilles: The non-existence of (3,1,2)-conjugate orthogonal idempotent Latin square of order 10 (2001)
- Bry, François; Yahya, Adnan: Positive unit hyperresolution tableaux and their application to minimal model generation (2000)
- Gent, I.; Stergiou, K.; Walsh, T.: Decomposable constraints (2000)
- Schumann, Johann M.: Automated theorem proving in software engineering. Foreword by Donald Loveland (2000)