2009 |
30 | EE | Peter Baumgartner,
Alexander Fuchs,
Hans de Nivelle,
Cesare Tinelli:
Computing finite models by reduction to function-free clause logic.
J. Applied Logic 7(1): 58-74 (2009) |
2008 |
29 | EE | Hans de Nivelle,
Piotr Witkowski:
A Small Framework for Proof Checking.
PAAR/ESHOL 2008 |
2006 |
28 | EE | Hans de Nivelle,
Jia Meng:
Geometric Resolution: A Proof Procedure Based on Finite Model Search.
IJCAR 2006: 303-317 |
2005 |
27 | EE | Hans de Nivelle,
Ruzica Piskac:
Verification of an Off-Line Checker for Priority Queues.
SEFM 2005: 210-219 |
26 | EE | Hans de Nivelle:
Translation of resolution proofs into short first-order proofs without choice axioms.
Inf. Comput. 199(1-2): 24-54 (2005) |
25 | EE | Stéphane Demri,
Hans de Nivelle:
Deciding Regular Grammar Logics with Converse Through First-Order Logic.
Journal of Logic, Language and Information 14(3): 289-329 (2005) |
2004 |
24 | EE | Yevgeny Kazakov,
Hans de Nivelle:
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
IJCAR 2004: 122-136 |
2003 |
23 | EE | Hans de Nivelle:
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms.
CADE 2003: 365-379 |
22 | EE | Yevgeny Kazakov,
Hans de Nivelle:
Subsumption of Concepts in FL0y for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete.
Description Logics 2003 |
21 | EE | Stéphane Demri,
Hans de Nivelle:
Deciding regular grammar logics with converse through first-order logic
CoRR cs.LO/0306117: (2003) |
20 | EE | Hans de Nivelle,
Maarten de Rijke:
Deciding the guarded fragments by resolution.
J. Symb. Comput. 35(1): 21-58 (2003) |
2002 |
19 | EE | Hans de Nivelle:
Extraction of Proofs from the Clausal Normal Form Transformation.
CSL 2002: 584-598 |
18 | | Marc Bezem,
Dimitri Hendriks,
Hans de Nivelle:
Automated Proof Construction in Type Theory Using Resolution.
J. Autom. Reasoning 29(3-4): 253-275 (2002) |
2001 |
17 | EE | Hans de Nivelle,
Ian Pratt-Hartmann:
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality.
IJCAR 2001: 211-225 |
16 | EE | Hans de Nivelle:
Splitting Through New Proposition Symbols.
LPAR 2001: 172-185 |
15 | EE | Carlos Areces,
Maarten de Rijke,
Hans de Nivelle:
Resolution in Modal, Description and Hybrid Logic.
J. Log. Comput. 11(5): 717-736 (2001) |
2000 |
14 | | Marc Bezem,
Dimitri Hendriks,
Hans de Nivelle:
Automated Proof Construction in Type Theory Using Resolution.
CADE 2000: 148-163 |
13 | | Hans de Nivelle:
Deciding the E+ - class by an a posteriori, liftable order.
Ann. Pure Appl. Logic 104(1-3): 219-232 (2000) |
12 | EE | Ullrich Hustadt,
Hans de Nivelle,
Renate A. Schmidt:
Resolution-Based Methods for Modal Logics.
Logic Journal of the IGPL 8(3): (2000) |
1999 |
11 | EE | Carlos Areces,
Hans de Nivelle,
Maarten de Rijke:
Prefixed Resolution: A Resolution Method for Modal and Description Logics.
CADE 1999: 187-201 |
10 | EE | Harald Ganzinger,
Hans de Nivelle:
A Superposition Decision Procedure for the Guarded Fragment with Equality.
LICS 1999: 295-304 |
1998 |
9 | EE | Hans de Nivelle:
A Resolution Decision Procedure for the Guarded Fragment.
CADE 1998: 191-204 |
8 | | Hans de Nivelle:
An Algorithm for the Retrieval of Unifiers from Discrimination Trees.
J. Autom. Reasoning 20(1): 5-25 (1998) |
7 | | Hans de Nivelle:
The Resolution Calculus, Alexander Leitsch.
Journal of Logic, Language and Information 7(4): 499-502 (1998) |
1997 |
6 | | Hans de Nivelle:
A Classification of Non-liftable Orders for Resolution.
CADE 1997: 336-350 |
1996 |
5 | | Hans de Nivelle:
An Algorithm for the Retrieval of Unifiers from Discrimination Trees.
JELIA 1996: 18-33 |
1994 |
4 | | Hans de Nivelle:
Resolution Games and Non-Liftable Resolution Orderings.
CSL 1994: 279-293 |
3 | | Cees Witteveen,
Wiebe van der Hoek,
Hans de Nivelle:
Revision of Non-Monotonic Theories.
JELIA 1994: 137-151 |
2 | | Hans de Nivelle:
A Unification of Ordering Refinements of Resolution in Classical Logic.
JELIA 1994: 217-230 |
1993 |
1 | | Hans de Nivelle:
Generic Resolution in Propositional Modal Systems.
LPAR 1993: 241-252 |