Homepage of Hans de Nivelle
address and email .
Homepage of the
institute .
Teaching
Master/Bachelor Projects
I have lots of interesting topics for master or bachelor thesis
in the areas of theorem proving and verification, and application of
those to airplane theory. Projects can be theoretical, or more
programmingoriented.
Research
My research interests are
automated theorem proving,
verification,
proof theory,
and
implementation.
Committee Memberships
Software
Geo
woke up from its sleep!
TABLEAUX/FroCoS 2015
I organized
TABLEAUX
and
FroCoS
in Wroclaw during 2124 September 2015.
Quaternion Finder
Build your own Quaternion Finder!
Thanks to Tomasz Wierzicki 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).
Summary in Polish /
in English.