| A superposition decision procedure for the guarded fragment with equality H Ganzinger, H De Nivelle Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158 …, 1999 | 152 | 1999 |
| Inference and computational semantics P Blackburn, J Bos, M Kohlhase, H De Nivelle Computing Meaning: Volume 2, 11-28, 2001 | 123 | 2001 |
| Resolution-based methods for modal logics H De Nivelle, RA Schmidt, U Hustadt Logic Journal of the IGPL 8 (3), 265-292, 2000 | 110 | 2000 |
| Computing finite models by reduction to function-free clause logic P Baumgartner, A Fuchs, H De Nivelle, C Tinelli Journal of Applied Logic 7 (1), 58-74, 2009 | 95 | 2009 |
| Deciding regular grammar logics with converse through first-order logic S Demri, H De Nivelle Journal of Logic, Language and Information 14, 289-329, 2005 | 73 | 2005 |
| Geometric resolution: A proof procedure based on finite model search H De Nivelle, J Meng International Joint Conference on Automated Reasoning, 303-317, 2006 | 70 | 2006 |
| Resolution in modal, description and hybrid logic C Areces, M de Rijke, H de Nivelle Journal of Logic and Computation 11 (5), 717-736, 2001 | 69 | 2001 |
| A resolution decision procedure for the guarded fragment H De Nivelle International Conference on Automated Deduction, 191-204, 1998 | 57 | 1998 |
| Ordering refinements of resolution. JMGG De Nivelle | 55 | 1997 |
| Automated proof construction in type theory using resolution M Bezem, D Hendriks, H De Nivelle Journal of Automated Reasoning 29 (3-4), 253, 2002 | 53 | 2002 |
| Deciding the guarded fragments by resolution H De Nivelle, M De Rijke Journal of Symbolic Computation 35 (1), 21-58, 2003 | 52 | 2003 |
| Subsumption of concepts in for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete Y Kazakov, H De Nivelle Max-Planck-Institut für Informatik, 2003 | 34 | 2003 |
| A resolution-based decision procedure for the two-variable fragment with equality H De Nivelle, I Pratt-Hartmann International Joint Conference on Automated Reasoning, 211-225, 2001 | 31 | 2001 |
| Splitting through new proposition symbols H de Nivelle International Conference on Logic for Programming Artificial Intelligence …, 2001 | 23 | 2001 |
| Prefixed resolution: A resolution method for modal and description logics H Ganzinger, C Areces, H de Nivelle, M de Rijke Automated Deduction—CADE-16: 16th International Conference on Automated …, 1999 | 22 | 1999 |
| Resolution games and non-liftable resolution orderings H de Nivelle International Workshop on Computer Science Logic, 279-293, 1994 | 20 | 1994 |
| Automated proof construction in type theory using resolution M Bezem, D Hendriks, H de Nivelle Automated Deduction-CADE-17: 17th International Conference on Automated …, 2000 | 19 | 2000 |
| Bliksem 1.10 user manual H De Nivelle MPI Saarbruecken, 1999 | 19 | 1999 |
| Translation of resolution proofs into short first-order proofs without choice axioms H de Nivelle Information and Computation 199 (1-2), 24-54, 2005 | 17 | 2005 |
| A resolution decision procedure for the guarded fragment with transitive guards Y Kazakov, H De Nivelle Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork …, 2004 | 17 | 2004 |
