Peter Backeman

Uppsala University, Sweden

PhD student working with automated theorem provers and SMT-solvers, focusing on quantifier handling in first-order logics.


Uppsala University

PhD in Computer Science

Supervisor Philipp Rümmer

November 2013 -

Uppsala University

Master of Science
Computer Science

Minor in Japanese

August 2010 - September 2013

Waseda University

Intesive Japanese Language Program

JLPT level 3 awarded.

September 2011 - June 2012

Uppsala University

Bachelor of Science
Computer Science

Minor in Chinese

August 2007 - June 2010


Introduction to IT

Teachers Assistant on the introductions course to the Computer Science program spanning on a wide variety of topics.

Fall 2014, 2015, 2016, 2017, (2018)

Machine Learning

Assisting students in lab exercises and project using various machine learning techniques (e.g., neural networks, reinforcement learning).

Spring 2015, 2016, 2018

Program Construction and Data Structures

Teachers Assistant on the introductory course to programming, using SML, for freshman students in the Computer Science program.

Autumn/Spring 2013/2014

Object-Oriented Development

Teachers Assistant an a distance course about object-oriented development using Java.

Spring 2014


Bounded Rigid E-Unification
Bounded Rigid E-Unification (BREU) is a restriction of regular E-Unification which was developed as a sub-procedure in a sequent based theorem prover (ePrincess). It is available as a separate library at GitHub implemented in Scala


ePrincess is a branch of the Princess theorem prover which utilises BREU as its unification procedure.


UppSAT is an approximating SMT-solver designed to allow for rapid prototyping and implementation of approximation of various theories. The latest version and documentation can be found at GitHub.


When not solving real problems I enjoy solving puzzles and riddles. Both more old-fashioned ones, but also more programming-oriented. I also enjoy programming contests (albeit in a less competative manner) and have partook in the Nordic Collegiate Programming Contest a few times (best placing 43rd in total, 17th in Sweden).

When not focusing on problem-solving I like to watch movies and read books, especially non-fiction. I strongly recommend anyone who hasn't read either Sapiens or Thinking, Fast and Slow, to give them a go!

I am also fascinated by teaching in its various forms. Previously, I have been engaged in Coaching Maths Online and in an pre-introducationary course for new computer science students. Now, I have the chance of exploring this both as a TA on various courses, as well as in my day-to-day life together with my child.