Mechanizing Complemented Lattices Within Mizar Type System
Adam Grabowski · Journal of Automated Reasoning · 2015
Recently some longstanding open lattice theory problems were solved with the help of automated theorem provers. The question which may be posed is how to cope with such results to improve their presentation for human without loss of machine-readability, not only at the proof level, which should be rather straightforward, but also at the stage of rebuilding appropriate data structure. We describe the framework extending already existed in the Mizar library for Boolean algebras to cover more general cases of lattice with complements. The efficiency of this approach was tested e.g. on short axiom systems for Boolean algebras based on negation and disjunction. We also proved Nachbin theorem for spectra of distributive lattices.