Generic Resolution in Propositional Modal Systems. - Hans de Nivelle (LPAR, 1993)

Resolution Games and Non-Liftable Resolution Orderings. - Hans de Nivelle (CSL, 1994)

A Unification of Ordering Refinements of Resolution in Classical Logic. - Hans de Nivelle (JELIA, 1994)

Revision of Non-Monotonic Theories. - Cees Witteveen; Wiebe van der Hoek; Hans de Nivelle (JELIA, 1994)

A Classification of Non-liftable Orders for Resolution. - Hans de Nivelle (CADE, 1997)

A Resolution Decision Procedure for the Guarded Fragment. - Hans de Nivelle (CADE, 1998)

An Algorithm for the Retrieval of Unifiers from Discrimination Trees. - Hans de Nivelle (J. Autom. Reason., 1998)

The Resolution Calculus, Alexander Leitsch. - Hans de Nivelle (J. Log. Lang. Inf., 1998)

Prefixed Resolution: A Resolution Method for Modal and Description Logics. - Carlos Areces; Hans de Nivelle; Maarten de Rijke (CADE, 1999)

A Superposition Decision Procedure for the Guarded Fragment with Equality. - Harald Ganzinger; Hans de Nivelle (LICS, 1999)

Deciding the E+ - class by an a posteriori, liftable order. - Hans de Nivelle (Ann. Pure Appl. Log., 2000)

Resolution-Based Methods for Modal Logics. - Ullrich Hustadt; Hans de Nivelle; Renate A. Schmidt (Log. J. IGPL, 2000)

A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. - Hans de Nivelle; Ian Pratt-Hartmann (IJCAR, 2001)

Splitting Through New Proposition Symbols. - Hans de Nivelle (LPAR, 2001)

Resolution in Modal, Description and Hybrid Logic. - Carlos Areces; Maarten de Rijke; Hans de Nivelle (J. Log. Comput., 2001)

Extraction of Proofs from the Clausal Normal Form Transformation. - Hans de Nivelle (CSL, 2002)

Automated Proof Construction in Type Theory Using Resolution. - Marc Bezem; Dimitri Hendriks; Hans de Nivelle (J. Autom. Reason., 2002)

Subsumption of Concepts in FL0y for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete. - Yevgeny Kazakov; Hans de Nivelle (Description Logics, 2003)

Deciding the guarded fragments by resolution. - Hans de Nivelle; Maarten de Rijke (J. Symb. Comput., 2003)

A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. - Yevgeny Kazakov; Hans de Nivelle (IJCAR, 2004)

Preface. - Wolfgang Ahrendt; Peter Baumgartner 001; Hans de Nivelle; Silvio Ranise; Cesare Tinelli (D/PDPAR@IJCAR, 2004)

Verification of an Off-Line Checker for Priority Queues. - Hans de Nivelle; Ruzica Piskac (SEFM, 2005)

Translation of resolution proofs into short first-order proofs without choice axioms. - Hans de Nivelle (Inf. Comput., 2005)

Deciding Regular Grammar Logics with Converse Through First-Order Logic. - Stéphane Demri; Hans de Nivelle (J. Log. Lang. Inf., 2005)

Geometric Resolution: A Proof Procedure Based on Finite Model Search. - Hans de Nivelle; Jia Meng 002 (IJCAR, 2006)

A Small Framework for Proof Checking. - Hans de Nivelle; Piotr Witkowski 001 (PAAR/ESHOL, 2008)

Computing finite models by reduction to function-free clause logic. - Peter Baumgartner 001; Alexander Fuchs 003; Hans de Nivelle; Cesare Tinelli (J. Appl. Log., 2009)

Classical Logic with Partial Functions. - Hans de Nivelle (J. Autom. Reason., 2011)

Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic. - Hans de Nivelle (ARQNL@IJCAR, 2014)

Theorem proving for classical logic with partial functions by reduction to Kleene logic. - Hans de Nivelle (J. Log. Comput., 2017)

Subsumption Algorithms for Three-Valued Geometric Resolution. - Hans de Nivelle (Log. Methods Comput. Sci., 2018)

Generating Tokenizers with Flat Automata. - Hans de Nivelle; Dina Muktubayeva (GandALF, 2022)