Alexander Anisimov: Bachelor's Thesis

Saarland University Computer Science

Proof Automation for Finite Sets

Advisors: Christian Doczkal, Gert Smolka
Supervisor: Gert Smolka

In this thesis we aim to provide proof automation for typed finite sets. To this intent, we consider three tableau calculi describing increasingly large fragments of set theory. The first one allows for reasoning about the basic set structures (union, difference, singleton, empty set) and relations. We prove total correctness for it. Our second calculus extends the first one by a powerset operator. It is still terminating, but we are not able to prove completeness anymore. The third calculus is even stronger and can express not only powersets but also separations. This system is no longer terminating. The decidability of the corresponding fragment of ZF set theory with untyped and possibly infinite sets is an open problem. So, it is likely that the decidability of our fragment is open, too.
For the full system we provide an implementation in Coq/Ssreflect. We consider the alternatives of a direct implementation in Ltac and a proof by computational reflection. The latter is appealing as it is often very efficient in practice. Studying it, we implement a naive decider for boolean tautologies and compare it with the trivial automation approaches. But, as reflection requires at least termination, we stick to a direct implementation in Ltac for our set automation.



Submitted on Aug 27, 2015 (PDF, Coq sources)


Legal notice, Privacy policy