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)
Tableau-Based Automation for Typed Finite Sets
Thesis
Submitted on Aug 27, 2015 (PDF, Coq sources)
References
-
Bernhard Beckert, Ulrike Hartmer: A Tableau Calculus for Quantifier-Free
Set Theoretic Formulae. TABLEAUX 1998: 93-107, Springer 1998
-
Samuel Boutin: Using Reflection to Build Efficient and Certified Decision
Procedures. TACS 1997: 515-529, 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:193-230, 1991, Springer 1991
-
Domenico Cantone, Calogero G. Zarba: A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory. FTP (LNCS
Selection) 1998: 126-136, Springer 2000
-
Domenico Cantone, Calogero G. Zarba: A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification. TABLEAUX 1999: 97-112, Springer 1999
-
Domenico Cantone, Rosa Ruggeri Cannata: Deciding set-theoretic 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): 49-72 (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.uni-saarland.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. 226-241, Springer, 2014
-
Alfredo Ferro, Eugenio G. Omodeo, Jacob T. Schwartz: Decision procedures
for some fragments of set theory. CADE 1980: 88-96, Springer 1980
-
Benjamin Shults: Comprehension and Description in Tableaux. 1997
-
Coq Development Team: Coq Documentation
https://coq.inria.fr/documentation
Legal notice, Privacy policy
