Bio

Jan Stańczuk is about to graduate with a bachelor of science in mathematics and computer science at King’s College London. He is very passionate about mathematics and intends to pursue a master’s in pure mathematics at Imperial College London next year. His mathematical interests range from logic, axiomatic set theory, topology and measure theory to applied probability and machine learning. Besides mathematics and computer science, Jan is deeply interested in physics, philosophy, music and martial arts.

Computational Essay: The Stone–Weierstrass Theorem

Project: Resolution Based Automated Theorem Prover for First Order Logic

Project Overview

In order to be able to apply the resolution method to an arbitrary sentence in first order logic, one must first convert it to conjunctive normal form (CNF). I began my project by implementing the necessary components of the conversion including conversion to prenex normal form and elimination of existential quantifiers using Skolemization. Afterwards, I implemented the most general unification algorithm, which is a central part of a resolution based theorem prover. Having all the components in place I implemented the resolution algorithms using two resolution strategies, Set of Support and Linear Resolution, thereby completing the implementation of the theorem prover. The resulting implementation provides a complete semi-decision procedure for first order logic. In principle given infinite time and memory the theorem prover could find a proof of any theorem entailed by the given set of axioms.