Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., et al. (eds.) Proc. of MKM 2011, LNCS, vol. 6824, pp. 149–163. Springer, Berlin, Heidelberg (2011)
Balbes, R., Dwinger, P.: Distributive Lattices. University of Missouri Press (1975)
Bancerek, G.: Development of the theory of continuous lattices in Mizar. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automatic Reasoning. The Calculemus-2000 Symposium, A K Peters, pp. 65–80 (2000)
Dahn, B.I.: Robbins algebras are Boolean: A revision of McCune’s computer-generated solution of Robbins problem. J. Algebra 208, 526–532 (1998)
Fitelson, B.: Using Mathematica 3.0 to understand the computer proof of the Robbins conjecture. Math. Ed. Res. 7(1) (1998)
Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271–286 (2002)
Grabowski, A.: Automated discovery of properties of rough sets. Fundamenta Informaticae 128(1–2), 65–79 (2013)
Grabowski, A.: Prime filters and ideals in distributive lattices, MML Id: LATTICEA. Formalized Mathematics 21(3), 213–221 (2013)
Grabowski, A.: Robbins algebras vs. Boolean algebras, MML Id: ROBBINS1. Formalized Mathematics 9(4), 681–690 (2001)
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reason. 3(2), 153–245 (2010)
Grabowski, A., Schwarzweller, Ch.: Revisions as an essential tool to maintain mathematical repositories. In: Proc. of the 14th symposium on Towards Mechanized Mathematical Assistants, MKM 2007, Hagenberg, Austria, LNCS, vol. 4573, pp. 235–249, Springer (2007)
Grabowski, A., Schwarzweller, Ch.: Towards automatically categorizing mathematical knowledge. In: Federated Conference on Computer Science and Information Systems – FedCSIS 2012, Wroclaw, Poland, 9–12 September 2012, Proceedings, pp. 63–68 (2012)
Grätzer, G.: Lattice Theory: Foundation. Birkhäuser (2011)
Huntington, E.V.: Boolean algebra: a correction. Trans. AMS 35(2), 557–558 (1933)
Huntington, E.V.: New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell’s Principia Mathematica. Trans. AMS 35, 274–304 (1933)
Kornilowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013)
McCune, W.: Solution of the Robbins problem. J. Autom. Reason. 19, 263–276 (1997)
McCune, W., Veroff, R., Fitelson, B., Harris, K., Feist, A., Wos, L.: Short single axioms for Boolean algebra. J. Autom. Reason. 29(1), 1–16 (2002)
Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010)
Naumowicz, A., Bylinski, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) Proc. of Third International Conference on Mathematical Knowledge Management, LNCS, vol. 3119, pp. 290–301. Springer (2004)
Naumowicz, A., Kornilowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings of TPHOLs’09, LNCS, vol. 5674, pp. 67–72. Springer, Berlin, Heidelberg (2009)
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: a proof assistant for higher order logic. Springer, Berlin (2002)
Pak, K.: Improving legibility of natural deduction proofs is not trivial. Logical Methods Comput. Sci. 10(3), 1–30 (2014)
Pak, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013)
Trybulec, A., Kornilowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013)
Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013)
zukowski, S.: Introduction to lattice theory, MML Id: LATTICES. Formalized Mathematics 1(1), 215–222 (1990)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Grabowski, A. Mechanizing Complemented Lattices Within Mizar Type System. J Autom Reasoning 55, 211–221 (2015). https://doi.org/10.1007/s10817-015-9333-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9333-5