Reasoning about algebraic structures with implicit carriers in Isabelle/HOL. (English) Zbl 07614673
Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 236-253 (2020).
Summary: We prove Chen and Grätzer’s construction theorem for Stone algebras in Isabelle/HOL. The development requires extensive reasoning about algebraic structures in addition to reasoning in algebraic structures. We present an approach for this using classes and locales with implicit carriers. This involves using function liftings to implement some aspects of dependent types and using embeddings of algebras to inherit theorems. We also formalise a theory of filters based on partial orders.
For the entire collection see [Zbl 1498.68017].
For the entire collection see [Zbl 1498.68017].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Software:
Lifting; Stone Algebras; Transfer; Archive Formal Proofs; Isabelle/HOL; Locales; SledgehammerReferences:
| [1] | Balbes, R., Dwinger, P.: Distributive Lattices. University of Missouri Press, Columbia (1974) · Zbl 0321.06012 |
| [2] | Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123-153 (2014) · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7 |
| [3] | Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV, 3rd edn. American Mathematical Society, Providence (1967) · Zbl 0153.02501 |
| [4] | Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116-130. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_11 · Zbl 1314.68271 · doi:10.1007/978-3-642-22438-6_11 |
| [5] | Blyth, T.S.: Lattices and Ordered Algebraic Structures. Springer, London (2005). https://doi.org/10.1007/b139095 · Zbl 1073.06001 · doi:10.1007/b139095 |
| [6] | Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer, New York (1981) · Zbl 0478.08001 · doi:10.1007/978-1-4613-8130-3 |
| [7] | Capretta, V.: Universal algebra in type theory. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 131-148. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_10 · Zbl 0947.08001 · doi:10.1007/3-540-48256-3_10 |
| [8] | Chen, C.C., Grätzer, G.: Stone lattices. I: Construction theorems. Can. J. Math. 21, 884-894 (1969) · Zbl 0184.03303 · doi:10.4153/CJM-1969-096-5 |
| [9] | Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002) · Zbl 1002.06001 · doi:10.1017/CBO9780511809088 |
| [10] | Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle/HOL. In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol. 6663, pp. 52-67. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21070-9_5 · Zbl 1329.68230 · doi:10.1007/978-3-642-21070-9_5 |
| [11] | Grätzer, G.: Lattice Theory: First Concepts and Distributive Lattices. W. H. Freeman and Co., New York (1971) · Zbl 0232.06001 |
| [12] | Grätzer, G., Schmidt, E.T.: On ideal theory for lattices. Acta Sci. Math. 19(1-2), 82-92 (1958) · Zbl 0092.26802 |
| [13] | Guttmann, W.: Stone algebras. Archive of Formal Proofs (2016) |
| [14] | Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theor. Comput. Sci. 744, 37-55 (2018) · Zbl 1401.68246 · doi:10.1016/j.tcs.2018.04.012 |
| [15] | Guttmann, W.: Verifying minimum spanning tree algorithms with Stone relation algebras. J. Log. Algebraic Methods Program. 101, 132-150 (2018) · Zbl 1401.68247 · doi:10.1016/j.jlamp.2018.09.005 |
| [16] | Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 160-174. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74464-1_11 · Zbl 1178.68529 · doi:10.1007/978-3-540-74464-1_11 |
| [17] | Horn, A.: On sentences which are true of direct unions of algebras. J. Symbol. Log. 16(1), 14-21 (1951) · Zbl 0043.24801 · doi:10.2307/2268661 |
| [18] | Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131-146. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_9 · Zbl 1426.68284 · doi:10.1007/978-3-319-03545-1_9 |
| [19] | Immler, F., Zhan, B.: Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. In: Mahboubi, A., Myreen, M.O. (eds.) CPP 2019, pp. 65-77. ACM (2019) |
| [20] | Johnsson, T.: Lambda lifting: transforming programs to recursive equations. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 190-203. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-15975-4_37 · Zbl 0568.68013 · doi:10.1007/3-540-15975-4_37 |
| [21] | Johnstone, P.T.: Stone Spaces. Cambridge University Press, Cambridge (1982) · Zbl 0499.54001 |
| [22] | Kammüller, F.: Modular structures as dependent types in Isabelle. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 121-133. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48167-2_9 · Zbl 0942.68116 · doi:10.1007/3-540-48167-2_9 |
| [23] | Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149-165. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_11 · doi:10.1007/3-540-48256-3_11 |
| [24] | Katriňák, T.: Die Kennzeichnung der distributiven pseudokomplementären Halbverbände. Journal für die reine und angewandte Mathematik 241, 160-179 (1970) · Zbl 0192.33503 |
| [25] | Katriňák, T.: A new proof of the construction theorem for Stone algebras. Proc. Am. Math. Soc. 40(1), 75-78 (1973) · Zbl 0258.06006 · doi:10.2307/2038636 |
| [26] | Katriňák, T., Mederly, P.: Constructions of p-algebras. Algebra Univers. 17(1), 288-316 (1983) · Zbl 0536.06004 · doi:10.1007/BF01194538 |
| [27] | Kunčar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237-260 (2018) · Zbl 1468.68295 · doi:10.1007/s10817-018-9464-6 |
| [28] | Nemitz, W.C.: Implicative semi-lattices. Trans. Am. Math. Soc. 117, 128-142 (1965) · Zbl 0128.24804 · doi:10.1090/S0002-9947-1965-0176944-9 |
| [29] | Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9 · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [30] | Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 3-13 (2010) |
| [31] | Polkowski, L.: Rough Sets: Mathematical Foundations. Springer, Heidelberg (2002). https://doi.org/10.1007/978-3-7908-1776-8 · Zbl 1040.68114 · doi:10.1007/978-3-7908-1776-8 |
| [32] | Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795-825 (2011) · Zbl 1223.68105 · doi:10.1017/S0960129511000119 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
