Paper Info
Title
Formalising Overlap Algebras in Matita.
Abstract
We describe some formal topological results, formalised in Matita 1/2, presented in predicative intuitionistic logic and in terms of Overlap Algebras. Overlap Algebras are new algebraic structures designed to ease reasoning about subsets in an algebraic way within intuitionistic logic. We find that they also ease the formalisation of formal topological results in an interactive theorem prover. Our main result is the existence of a functor between two categories of 'generalised topological spaces', one with points (Basic Pairs) and the other point-free (Basic Topologies). This formalisation is part of a wider scientific collaboration with the inventor of the theory, Giovanni Sambin. His goal is to verify in what sense his theory is 'implementable', and to discover what problems may arise in the process. We check that all intermediate constructions respect the stringent size requirements imposed by predicative logic. The formalisation is quite unusual, since it has to make explicit size information that is often hidden. We found that the version of Matita used for the formalisation was largely inappropriate. The formalisation drove several major improvements of Matita that will be integrated in the next major release (Matita 1.0). We show some motivating examples, taken directly from the formalisation, for these improvements. We also describe a possibly sub-optimal solution in Matita 1/2, which is exploitable in other similar systems. We briefly discuss a better solution available in Matita 1.0.
Year
DOI
Venue
2011
10.1017/S0960129511000107
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Algebra,Artificial intelligence,Mathematics
Journal
21
Issue
ISSN
Citations 
SP4
0960-1295
3
PageRank 
References 
Authors
0.41
12
2
Name
Order
Citations
PageRank
Claudio Sacerdoti Coen138440.66
Enrico Tassi232721.79