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]
Reinhard Pichler Speeding up Algorithms on Atomic Representations of Herbrand Models via New Redundancy Criteria. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 2000, v:29, n:2, pp:213-257 [Journal]
Marc Fuchs Controlled Use of Clausal Lemmas in Connection Tableau Calculi. [Citation Graph (0, 0)][DBLP] J. Symb. Comput., 2000, v:29, n:2, pp:299-341 [Journal]