Alexander Anisimov: Bachelor's Thesis
Proof Automation for Finite Sets
Advisors: Christian Doczkal, Gert Smolka
Supervisor: Gert Smolka
Abstract:
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.
Presentations

Initial talk: Feb 20, 2015 (slides)
Proof by Reflection and Automation for Boolean Logic

Second talk: May 08, 2015 (slides)
A Tableau System for Typed Finite Sets

Final talk: Sep 11, 2015 (slides)
TableauBased Automation for Typed Finite Sets
Thesis
Submitted on Aug 27, 2015 (PDF, Coq sources)
References

Bernhard Beckert, Ulrike Hartmer: A Tableau Calculus for QuantifierFree
Set Theoretic Formulae. TABLEAUX 1998: 93107, Springer 1998

Samuel Boutin: Using Reflection to Build Efficient and Certified Decision
Procedures. TACS 1997: 515529, Springer 1997

Domenico Cantone: Decision procedures for elementary sublanguages of
set theory: X. Multilevel syllogistic extended by the singleton and powerset
operators. J. Autom. Reasoning 7:193230, 1991, Springer 1991

Domenico Cantone, Calogero G. Zarba: A New Fast TableauBased Decision Procedure for an Unquantified Fragment of Set Theory. FTP (LNCS
Selection) 1998: 126136, Springer 2000

Domenico Cantone, Calogero G. Zarba: A TableauBased Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification. TABLEAUX 1999: 97112, Springer 1999

Domenico Cantone, Rosa Ruggeri Cannata: Deciding settheoretic formulae
with the predicate ’finite’ by a tableau calculus. Le Matematiche Vol 50, No 1 (1995)

Domenico Cantone, Calogero G. Zarba, Rosa Ruggeri Cannata: A Tableau
Based Decision Procedure for a Fragment of Set Theory with Iterated Membership. J. Autom. Reasoning 34(1): 4972 (2005), Springer 2005

Adam Chlipala: Certified Programming with Dependent Types (2014).
http://adam.chlipala.net/cpdt/

Christian Doczkal:
Finite Sets over Countalbe Types in Ssreflect
http://www.ps.unisaarland.de/formalizations/fset.php

Christian Doczkal, Gert Smolka Completeness and Decidability Results for
CTL in Coq Interactive Theorem Proving (ITP 2014), Vol. 8558 of LNAI,
pp. 226241, Springer, 2014

Alfredo Ferro, Eugenio G. Omodeo, Jacob T. Schwartz: Decision procedures
for some fragments of set theory. CADE 1980: 8896, Springer 1980

Benjamin Shults: Comprehension and Description in Tableaux. 1997

Coq Development Team: Coq Documentation
https://coq.inria.fr/documentation
Alexander Anisimov,
Fri Sep 11 16:35:50 2015