Hans de Nivelle was born in the Netherlands, and has Dutch nationality. He obtained his PhD in 1995 from Delft University of Technology.
Topic of his thesis was ‘Ordering Refinements of Resolution’. From 1996 until 1999, he worked at various places in the Netherlands, namely Tilburg, Delft and Amsterdam. From 1999 until 2007, Hans de Nivelle was senior researcher at the Max-Planck Institute for Computer Science in Saarbruecken, Germany.
From 2007 until 2017, he was professor at Computer Science Department of Wroclaw University in Poland.
In October 2017, he joined Nazarbayev University.
Programming in C++. It is a complex language, and if you don’t know how to use it, you will use it wrong. I teach how to write understandable, extendable code, which is reasonably efficient, as the designers of C++ intend it to be used.
Compiler Construction. This topic carries a nice mixture of theory and practice. One must understand formal language theory, type theory, and abstract interpretation. One must understand this at such level, that one cannot only talk about it, but also apply it in concrete examples.
Flight Simulation. One needs to be good at physics, and at implementation. First part of the course consists of modelling of point masses, planets and rockets. After that, we move to two dimensional airplanes (forward and up/down).
The last part of the course introduces a complete, three-dimensional airplane model.
I am interested in applying logic to the verification of mathematics and programs. My recent publications are about using three-valued logic for modeling functions that can fail (usually called `partial functions’). Examples are division by zero, or taking the value of a pointer that can be NULL. I study logics that can handle such functions. What is the best logic for such functions, how does one use this logic in practice, and how can one automatically find proofs in it?
Subsumption Algorithms for Three-Valued Geometric Resolution,
International Joint Conference on Automated Reasoning (IJCAR),
Theorem Proving for Classical Logic with Partial Functions by Reduction to Kleene Logic,
Journal of Logic and Computation 27(2), 2017.
Classical Logic with Partial Functions,
Journal of Automated Reasoning 47(4), 2011.
Computing Finite Models by Reduction to Function-Free Clause Logic,
Journal of Applied Logic 7(1), 2009.
Co-authored with Peter Baumgartner, Alexander Fuchs, and Cesare Tinelli.
Theorem prover Geo III, can be obtained from the CADE ATP
System Competition (CASC 2015).
It is an implementation of 3-valued logic.