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


Programming of Embedded Systems

Co-Course responsible, giving lectures and assisting students in programming embedded systems.

Fall 2019

Basic Programming with Didactic Specialisation for Teachers

Lecturing Python to grade-school mathematics teachers.

Fall 2019

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, 2019

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 for Presburger arithmetic which utilises BREU as its unification procedure. It competed in the 2015 year edition of casc (CASC-25) where it won prize for best newcomer.

Since then the underlying BREU library has been reworked and a reintegration into the latest version of Princess is work in progress.

Investigations has also been done how to incorporate BREU into a connection tableaux prover. If you are interested in running ePrincess, it is available as a JAR-file. If you are interested in the source code, please contact by e-mail.


UppSAT is an approximating SMT-solver designed to allow for rapid prototyping and implementation of approximation of various theories. All information is now located 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.