# Projects and Thesis Topics

Please contact
me if you are interested!

### Equation Handling in First-Order Logic with Integers

Automated theorem provers for first-order logic are important for a
number of applications, for instance for the analysis of software
programs and hardware designs, or to assist mechanised (fully
automatic, or partly interactive) reasoning about mathematical
theorems. A number of mature and highly efficient theorem provers have
been developed over the last decades.

In order to reason about equations within first-order logic formulae,
two main paradigms are applied by automated theorem provers: ordered
rewriting, and congruence closure [1]. The former method tends to be
successful for formulae that contain both equations and quantifiers,
and has been extended to yield approaches such as free variables,
unification [2], Knuth-Bendix completion, or superposition; the latter
method is primarily successful for quantifier-free problems, but easy
to combine with theory-reasoning, such as handling problems in (linear)
arithmetic or arrays. The combination of quantifiers and logical
theories is often considered challenging.

The topic of this Master's thesis is the combination of congruence
closure with first-order unification and free variables. The goal is to
create a procedure that is efficient both for formulae with
quantifiers, and for formulae over the theory of (linear) integer
arithmetic. The thesis will build on previous theoretic and
experimental work at the IT Department, Uppsala University, which in
particular led to the implementation of the first-order theorem prover
"Princess" that won in the TFA division
(arithmetic problems) at the
CASC J6 competition
in 2012.

The thesis work will include the following parts:

- Study of background and related work
- Investigation how unification algorithms (e.g., Robinson's
algorithm) can be reformulated within the framework of congruence
closure, augmented with free variables
- Implementation and experimental evaluation

Prerequisites: General knowledge about first-order logic, and if
possible automated reasoning

[1] Abstract congruence closure. Leo Bachmair, Ashish Tiwari,
Laurent Vigneron. Journal of Automated Reasoning, 2003

[2] Unification theory. Franz Baader, Wayne Snyder. Handbook of
Automated Reasoning, 2001

### Further
topics offered in our research group