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 . 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 , 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:
Prerequisites: General knowledge about first-order logic, and if possible automated reasoning
 Abstract congruence closure. Leo Bachmair, Ashish Tiwari,
Laurent Vigneron. Journal of Automated Reasoning, 2003
 Unification theory. Franz Baader, Wayne Snyder. Handbook of Automated Reasoning, 2001