| 2016 | CADE | Subsumption Algorithms for Three-Valued Geometric Resolution. | Hans de Nivelle |
| 2014 | CADE | Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic. | Hans de Nivelle |
| 2010 | CADE | Classical Logic with Partial Functions. | Hans de Nivelle |
| 2008 | CADE | A Small Framework for Proof Checking. | Hans de Nivelle, Piotr Witkowski |
| 2006 | CADE | Geometric Resolution: A Proof Procedure Based on Finite Model Search. | Hans de Nivelle, Jia Meng |
| 2005 | SEFM | Verification of an Off-Line Checker for Priority Queues. | Hans de Nivelle, Ruzica Piskac |
| 2004 | CADE | A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. | Yevgeny Kazakov, Hans de Nivelle |
| 2003 | CADE | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. | Hans de Nivelle |
| 2002 | CSL | Extraction of Proofs from the Clausal Normal Form Transformation. | Hans de Nivelle |
| 2001 | CADE | A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. | Hans de Nivelle, Ian Pratt-Hartmann |
| 2001 | LPAR | Splitting Through New Proposition Symbols. | Hans de Nivelle |
| 2000 | CADE | Automated Proof Construction in Type Theory Using Resolution. | Marc Bezem, Dimitri Hendriks, Hans de Nivelle |
| 1999 | CADE | Prefixed Resolution: A Resolution Method for Modal and Description Logics. | Carlos Areces, Hans de Nivelle, Maarten de Rijke |
| 1999 | LICS | A Superposition Decision Procedure for the Guarded Fragment with Equality. | Harald Ganzinger, Hans de Nivelle |
| 1998 | CADE | A Resolution Decision Procedure for the Guarded Fragment. | Hans de Nivelle |
| 1997 | CADE | A Classification of Non-liftable Orders for Resolution. | Hans de Nivelle |
| 1996 | JELIA | An Algorithm for the Retrieval of Unifiers from Discrimination Trees. | Hans de Nivelle |
| 1994 | CSL | Resolution Games and Non-Liftable Resolution Orderings. | Hans de Nivelle |
| 1994 | JELIA | A Unification of Ordering Refinements of Resolution in Classical Logic. | Hans de Nivelle |
| 1994 | JELIA | Revision of Non-Monotonic Theories. | Cees Witteveen, Wiebe van der Hoek, Hans de Nivelle |
| 1993 | LPAR | Generic Resolution in Propositional Modal Systems. | Hans de Nivelle |