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
148 1999 Inference and computational semantics P Blackburn, J Bos, M Kohlhase, H De Nivelle
Computing Meaning: Volume 2, 11-28, 2001
122 2001 Resolution-based methods for modal logics H De Nivelle, RA Schmidt, U Hustadt
Logic Journal of the IGPL 8 (3), 265-292, 2000
108 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
87 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
74 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
67 2001 Automated proof construction in type theory using resolution M Bezem, D Hendriks, H De Nivelle
Journal of Automated Reasoning 29 (3-4), 253, 2002
56 2002 Ordering refinements of resolution. JMGG De Nivelle
56 1997 A resolution decision procedure for the guarded fragment H De Nivelle
International Conference on Automated Deduction, 191-204, 1998
55 1998 Deciding the guarded fragments by resolution H De Nivelle, M De Rijke
Journal of Symbolic Computation 35 (1), 21-58, 2003
51 2003 Subsumption of concepts in Y Kazakov, H De Nivelle
Max-Planck-Institut für Informatik, 2003
36 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
22 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
20 1999 Resolution games and non-liftable resolution orderings H de Nivelle
International Workshop on Computer Science Logic, 279-293, 1994
20 1994 Bliksem 1.10 user manual H De Nivelle
MPI Saarbruecken, 1999
19 1999 Extraction of proofs from the clausal normal form transformation H de Nivelle
International Workshop on Computer Science Logic, 584-598, 2002
18 2002 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
18 2000 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 