Hans de Nivelle Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. [Citation Graph (0, 0)][DBLP] CADE, 2003, pp:365-379 [Conf]
Yevgeny Kazakov, Hans de Nivelle Subsumption of Concepts in FL0y for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete. [Citation Graph (0, 0)][DBLP] Description Logics, 2003, pp:- [Conf]
Hans de Nivelle A Unification of Ordering Refinements of Resolution in Classical Logic. [Citation Graph (0, 0)][DBLP] JELIA, 1994, pp:217-230 [Conf]
Hans de Nivelle Deciding the E+ - class by an a posteriori, liftable order. [Citation Graph (0, 0)][DBLP] Ann. Pure Appl. Logic, 2000, v:104, n:1-3, pp:219-232 [Journal]
Hans de Nivelle Translation of resolution proofs into short first-order proofs without choice axioms. [Citation Graph (0, 0)][DBLP] Inf. Comput., 2005, v:199, n:1-2, pp:24-54 [Journal]
Hans de Nivelle An Algorithm for the Retrieval of Unifiers from Discrimination Trees. [Citation Graph (0, 0)][DBLP] J. Autom. Reasoning, 1998, v:20, n:1, pp:5-25 [Journal]
Stéphane Demri, Hans de Nivelle Deciding Regular Grammar Logics with Converse Through First-Order Logic. [Citation Graph (0, 0)][DBLP] Journal of Logic, Language and Information, 2005, v:14, n:3, pp:289-329 [Journal]
Hans de Nivelle The Resolution Calculus, Alexander Leitsch. [Citation Graph (0, 0)][DBLP] Journal of Logic, Language and Information, 1998, v:7, n:4, pp:499-502 [Journal]