Faculty Members
Hans de Nivelle, School of Science and Techology
Research Interests
My research interests are automated theorem proving, verification, proof theory, and implementation.
Committee Memberships
 IJCAR 2018, Oxford, UK, 1417 July 2018.
 Member of the TABLEAUX steering committee.
Past Committee Memberhips
 TABLEAUX 2017, Brasilia, 2529 september 2017.
 CADE 26, Gothenburg, 611 August 2017.
Teaching
For teaching, I refer to my previous homepage in Wroclaw.
Conferences Organized
I organized CADE 23, TABLEAUX 2015, and FroCoS 2015 in Wroclaw, Poland.
Quaternion Finder
Build your own Quaternion Finder! Thanks to Tomasz Wierzbicki for the typesetting.
The cube can also be used for finding (the rotations of) transformations between different coordinate systems as follows:
 Align the cube with coordinate system C1.
 Find the position of (1;0,0,0) on the cube.
 Align the cube with coordinate system C2.
 The quaternion can be read off from the place where (1;0,0,0) was found in Step 2.
Example
What quaternion represents the eye coordinates of a pilot, relative to the coordinate system of his plane?
Assume that you are the pilot. Airplane coordinates have X pointing forward, Y to the right, Z down. In this orientation, (1;0,0,0) is at the bottom of the cube to the right.
In your eye coordinates, X will be to the right, Y will be upwards, Z will be pointing behind you. If you align the cube, bottom right now contains the quaternion (1;1,1,1).
Grants

Holder of NCN (Narodowe Centrum Nauki) grant ‘Decision Procedures for Verification’ (DEC2011/03/B/ST6/00346), together with Witold Charatonik.

Started on 01.03.2016: Zastosowania logiki z funcjami częściowymi. (Applications of Logic with Partial Functions). In Polish / In English.