# Homepage of Hans de Nivelle

address and email . Homepage of the institute .

## Teaching

In October 2017, I will move to the School of Science and Technology of Nazarbayev University in Astana, where I will probably teach a course on Data Structures and Algorithms. This means that I will not be teaching in Wrocław any more. Here is an overview of lectures that I taught in Wrocław.

## Research

My research interests are automated theorem proving, verification, proof theory, and implementation.

## Software

Geo woke up from its sleep!

## TABLEAUX/FroCoS 2015

I organized TABLEAUX and FroCoS in Wroclaw during 21-24 September 2015.

## Quaternion Finder

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:

1. Align the cube with coordinate system C1.
2. Find the position of (1;0,0,0) on the cube.
3. Align the cube with coordinate system C2.
4. 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' (DEC-2011/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.