Hans de Nivelle

Publication Activity (10 Years)

Years Active: 1993-2022
Publications (10 Years): 5

Top Topics

Theorem Proving

Computationally Efficient

Classical Logic

Top Venues

J. Log. Comput.

Publications

Hans de Nivelle, Dina Muktubayeva
Generating Tokenizers with Flat Automata. GandALF (2022)
Hans de Nivelle
Subsumption Algorithms for Three-Valued Geometric Resolution. Log. Methods Comput. Sci. 14 (4) (2018)
Hans de Nivelle
Subsumption Algorithms for Three-Valued Geometric Resolution. CoRR (2017)
Hans de Nivelle
Theorem proving for classical logic with partial functions by reduction to Kleene logic. J. Log. Comput. 27 (2) (2017)
Hans de Nivelle
Subsumption Algorithms for Three-Valued Geometric Resolution. IJCAR (2016)
Hans de Nivelle
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic. ARQNL@IJCAR (2014)
Hans de Nivelle
Classical Logic with Partial Functions. J. Autom. Reason. 47 (4) (2011)
Hans de Nivelle
Classical Logic with Partial Functions. IJCAR (2010)
Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli
Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7 (1) (2009)
Hans de Nivelle, Piotr Witkowski
A Small Framework for Proof Checking. PAAR/ESHOL (2008)
Hans de Nivelle, Jia Meng
Geometric Resolution: A Proof Procedure Based on Finite Model Search. IJCAR (2006)
Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli
Preface. Electron. Notes Theor. Comput. Sci. 125 (3) (2005)
Hans de Nivelle
Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199 (1-2) (2005)
Stéphane Demri, Hans de Nivelle
Deciding Regular Grammar Logics with Converse Through First-Order Logic. J. Log. Lang. Inf. 14 (3) (2005)
Hans de Nivelle, Ruzica Piskac
Verification of an Off-Line Checker for Priority Queues. SEFM (2005)
Yevgeny Kazakov, Hans de Nivelle
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. IJCAR (2004)
Hans de Nivelle
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. CADE (2003)
Hans de Nivelle, Maarten de Rijke
Deciding the guarded fragments by resolution. J. Symb. Comput. 35 (1) (2003)
Yevgeny Kazakov, Hans de Nivelle
for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete. Description Logics (2003)
Stéphane Demri, Hans de Nivelle
Deciding regular grammar logics with converse through first-order logic CoRR (2003)
Marc Bezem, Dimitri Hendriks, Hans de Nivelle
Automated Proof Construction in Type Theory Using Resolution. J. Autom. Reason. 29 (3-4) (2002)
Hans de Nivelle
Extraction of Proofs from the Clausal Normal Form Transformation. CSL (2002)
Hans de Nivelle
Splitting Through New Proposition Symbols. LPAR (2001)
Hans de Nivelle, Ian Pratt-Hartmann
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. IJCAR (2001)
Carlos Areces, Maarten de Rijke, Hans de Nivelle
Resolution in Modal, Description and Hybrid Logic. J. Log. Comput. 11 (5) (2001)
Marc Bezem, Dimitri Hendriks, Hans de Nivelle
Automated Proof Construction in Type Theory Using Resolution. CADE (2000)
Hans de Nivelle
- class by an a posteriori, liftable order. Ann. Pure Appl. Log. 104 (1-3) (2000)
Ullrich Hustadt, Hans de Nivelle, Renate A. Schmidt
Resolution-Based Methods for Modal Logics. Log. J. IGPL 8 (3) (2000)
Carlos Areces, Hans de Nivelle, Maarten de Rijke
Prefixed Resolution: A Resolution Method for Modal and Description Logics. CADE (1999)
Harald Ganzinger, Hans de Nivelle
A Superposition Decision Procedure for the Guarded Fragment with Equality. LICS (1999)
Hans de Nivelle
A Resolution Decision Procedure for the Guarded Fragment. CADE (1998)
Hans de Nivelle
An Algorithm for the Retrieval of Unifiers from Discrimination Trees. J. Autom. Reason. 20 (1) (1998)
Hans de Nivelle
The Resolution Calculus, Alexander Leitsch. J. Log. Lang. Inf. 7 (4) (1998)
Hans de Nivelle
A Classification of Non-liftable Orders for Resolution. CADE (1997)
Hans de Nivelle
An Algorithm for the Retrieval of Unifiers from Discrimination Trees. JELIA (1996)
Hans de Nivelle
A Unification of Ordering Refinements of Resolution in Classical Logic. JELIA (1994)
Cees Witteveen, Wiebe van der Hoek, Hans de Nivelle
Revision of Non-Monotonic Theories. JELIA (1994)
Hans de Nivelle
Resolution Games and Non-Liftable Resolution Orderings. CSL (1994)
Hans de Nivelle
Generic Resolution in Propositional Modal Systems. LPAR (1993)