Nicolas Peltier A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models. [Citation Graph (0, 0)][DBLP] TABLEAUX, 2003, pp:181-195 [Conf]
Nicolas Peltier Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models. [Citation Graph (0, 0)][DBLP] TABLEAUX, 1997, pp:313-327 [Conf]
Nicolas Peltier A Resolution-based Model Building Algorithm for a Fragment of OCC1N=. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2003, v:86, n:1, pp:- [Journal]
Nicolas Peltier Constructing Decision Procedures in Equational Clausal Logic. [Citation Graph (0, 0)][DBLP] Fundam. Inform., 2003, v:54, n:1, pp:17-65 [Journal]
Nicolas Peltier Pruning the Search Space and Extracting More Models in Tableaux. [Citation Graph (0, 0)][DBLP] Logic Journal of the IGPL, 1999, v:7, n:2, pp:217-251 [Journal]
Nicolas Peltier Representing and Building Models for Decidable Subclasses of Equational Clausal Logic. [Citation Graph (0, 0)][DBLP] J. Autom. Reasoning, 2004, v:33, n:2, pp:133-170 [Journal]
Nicolas Peltier Some Techniques for Proving Termination of the Hyperresolution Calculus. [Citation Graph (0, 0)][DBLP] J. Autom. Reasoning, 2005, v:35, n:4, pp:391-427 [Journal]
Ricardo Caferra, Nicolas Peltier Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 2000, v:29, n:2, pp:177-211 [Journal]
Nicolas Peltier Model building with ordered resolution: extracting models from saturated clause sets. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 2003, v:36, n:1-2, pp:5-48 [Journal]
Nicolas Peltier A calculus combining resolution and enumeration for building finite models. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 2003, v:36, n:1-2, pp:49-77 [Journal]
Nicolas Peltier Increasing Model Building Capabilities by Constraint Solving on Terms with Integer Exponents. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 1997, v:24, n:1, pp:59-101 [Journal]
Nicolas Peltier A New Method for Automated Finite Model Building Exploiting Failures and Symmetries. [Citation Graph (0, 0)][DBLP] J. Log. Comput., 1998, v:8, n:4, pp:511-543 [Journal]
Nicolas Peltier The first order theory of primal grammars is decidable. [Citation Graph (0, 0)][DBLP] Theor. Comput. Sci., 2004, v:323, n:1-3, pp:267-320 [Journal]