{"entities":{"Q7361763":{"pageid":31520828,"ns":120,"title":"Item:Q7361763","lastrevid":105368939,"modified":"2026-10-07T13:37:40Z","type":"item","id":"Q7361763","labels":{"en":{"language":"en","value":"Kleene Algebra"}},"descriptions":{"en":{"language":"en","value":"AFP entry Kleene_Algebra"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e025c136397ce5d3bf36111c805b46ef1956884d","datavalue":{"value":"https://isa-afp.org/entries/Kleene_Algebra.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361763$1BE7F074-3EA1-4D88-B7E9-5BF46699DC43","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"421496a141fb0326412f04e59c431545a872e1c1","datavalue":{"value":{"time":"+2013-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361763$02CF2679-3F86-4085-A2FA-7BA766AF65AA","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a4dbfcbe3ae3d36e41d2050bf2f236247628049c","datavalue":{"value":"Alasdair Armstrong","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361763$F3CA1E54-C580-4AE1-93BD-A2E150E3935C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"791c9af3f632028a8094f425e13128d157950d83","datavalue":{"value":"Georg Struth","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361763$6D243956-C81E-47E0-AFE9-2F94D0547427","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2f854883aaf7cde2ebd962b9b518c74b730cb624","datavalue":{"value":"Tjark Weber","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361763$20CF3CA6-C90F-447D-A5C5-C26ADEA6A330","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a270cda9b66de4f914a2f9952e1dc8e7871bd2af","datavalue":{"value":{"text":"Kleene Algebra","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361763$B37DD756-A67E-45AB-8129-77958598AB89","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f9cb3a35bb225babecffc3cbe7643a8e77686136","datavalue":{"value":"These files contain a formalisation of variants of Kleene algebras and their most important models as axiomatic type classes in Isabelle/HOL. Kleene algebras are foundational structures in computing with applications ranging from automata and language theory to computational modeling, program construction and verification. We start with formalising dioids, which are additively idempotent semirings, and expand them by axiomatisations of the Kleene star for finite iteration and an omega operation for infinite iteration. We show that powersets over a given monoid, (regular) languages, sets of paths in a graph, sets of computation traces, binary relations and formal power series form Kleene algebras, and consider further models based on lattices, max-plus semirings and min-plus semirings. We also demonstrate that dioids are closed under the formation of matrices (proofs for Kleene algebras remain to be completed). On the one hand we have aimed at a reference formalisation of variants of Kleene algebras that covers a wide range of variants and the core theorems in a structured and modular way and provides readable proofs at text book level. On the other hand, we intend to use this algebraic hierarchy and its models as a generic algebraic middle-layer from which programming applications can quickly be explored, implemented and verified.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361763$F3E23942-7901-4BF5-859A-8035EC44CC11","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b2e611a60bbb1cbb1ab23d8301e40dbbe2b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2915136,"id":"Q2915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$8FD7B207-54BA-47A7-9AF2-7F809FEBD34F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e68522e480793ad08c3035e092f5d824e5fae6d","datavalue":{"value":{"entity-type":"item","numeric-id":3783521,"id":"Q3783521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$D746C883-D239-4A0E-9748-E7C771ACCDCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a7f95a181a122f35ae18fd86fcaee76950d7cde","datavalue":{"value":{"entity-type":"item","numeric-id":5532570,"id":"Q5532570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$C0826676-481D-42A3-8FE2-3B05EC961D91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e375c52511dfb34f82e104f95edb5056ad3d650","datavalue":{"value":{"entity-type":"item","numeric-id":3479525,"id":"Q3479525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$59A3CB98-D21F-40F9-8CFC-3525E711A609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75e20f649ee163fc027b520d68f4bd0a0844cef5","datavalue":{"value":{"entity-type":"item","numeric-id":2721093,"id":"Q2721093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$6D6843A6-872E-4CA2-A95D-67356EBD7E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c95887997d61befa174dc6f5c2a08804d32a7d64","datavalue":{"value":{"entity-type":"item","numeric-id":5639639,"id":"Q5639639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$66157378-4E4B-4907-BAAE-BBFC3A2109B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e12fe299e2acf1d80201c464e52b99b82f6c1b5e","datavalue":{"value":{"entity-type":"item","numeric-id":3630173,"id":"Q3630173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$33CA0E6A-3207-42C7-8F94-09692A4633D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c08dc42b0e7ff775d175e9650bc18837bb9e6bc1","datavalue":{"value":{"entity-type":"item","numeric-id":5277765,"id":"Q5277765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$79F7D963-D278-4FF9-BABB-414518F139B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b90ce2baffc43563f7c49b8f5f238edbcb4e1d8b","datavalue":{"value":{"entity-type":"item","numeric-id":1391737,"id":"Q1391737"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$365C3799-1F31-4CEF-BD3C-B40EEC7B2F9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d033b0480cb3f4fe29c5cd97ee8fdad8a665383","datavalue":{"value":{"entity-type":"item","numeric-id":2908498,"id":"Q2908498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$2426516D-FA10-472C-BA54-E2CD3498C9B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca23da055412797c29f8737a832166566f69c4c4","datavalue":{"value":{"entity-type":"item","numeric-id":3007567,"id":"Q3007567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$C4F17296-E32F-4689-93B0-DD5B4805442F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b66c44c4ef6ee160003d0a07de5db4cffbce968f","datavalue":{"value":{"entity-type":"item","numeric-id":881452,"id":"Q881452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$2BD5D2A7-43CD-46AB-915D-711FD0A71DA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2790188d3a2572a99d3b8280868598d27c040965","datavalue":{"value":{"entity-type":"item","numeric-id":4525781,"id":"Q4525781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$95E2B1D5-DBE8-4FE6-9899-31C6BAD8C7D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"360383bb8da6b25f21760984236c3aab0e481c29","datavalue":{"value":{"entity-type":"item","numeric-id":604456,"id":"Q604456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$69B29E20-51B5-47FD-9104-7A5C2975F121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e13d4d25d9b41b80813e9e3772d78e6f24c19a44","datavalue":{"value":{"entity-type":"item","numeric-id":5738898,"id":"Q5738898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$FB10A15C-614B-4DD9-82E1-C67E02CA2213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcc11302650095b8014b4cfac23c2bd493ca57fc","datavalue":{"value":{"entity-type":"item","numeric-id":3358736,"id":"Q3358736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$AC3DE520-05C6-47B7-AB78-BF9D877146C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7ecdcca463445112101708876695eded3f30222","datavalue":{"value":{"entity-type":"item","numeric-id":1327385,"id":"Q1327385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$678A3C65-73FD-4395-AC87-CA4F3DB04AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83dd7302ae5c6ff14c7d7d4f9e7c2537339e8f91","datavalue":{"value":{"entity-type":"item","numeric-id":2392416,"id":"Q2392416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$C8A6309E-8D4F-4707-951D-E07D9BCBF09A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35e70c7ea0ca2c1202e957f84568392d9e230059","datavalue":{"value":{"entity-type":"item","numeric-id":5387864,"id":"Q5387864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$F37B0CCD-16E4-47F8-8844-44DAC94351D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6560cb7faf7ddacbb3391ec3e97070336eb2cb9d","datavalue":{"value":{"entity-type":"item","numeric-id":3671335,"id":"Q3671335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$CEAB65FD-0FF4-4F28-909A-9579C59D2F77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72a974f637709b7c0bbe6bc15d0ab90624a923b2","datavalue":{"value":{"entity-type":"item","numeric-id":4287490,"id":"Q4287490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$D909618B-BDA0-49AA-8B91-4C7CFE1BF4E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db93140569675f5c8c07160bf09fb1adedae60f7","datavalue":{"value":{"entity-type":"item","numeric-id":549683,"id":"Q549683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$88EED898-2DC6-406C-A823-CC1F616541E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a6daed1a8fcaca7a71aaae67ae286b4fdbaf987","datavalue":{"value":{"entity-type":"item","numeric-id":817587,"id":"Q817587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$CC763C6D-27D4-4BC5-953C-68F0FC9049B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4736b8f52d3360a8824f86f9655f4169ce694d1a","datavalue":{"value":{"entity-type":"item","numeric-id":1931903,"id":"Q1931903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$8055A0A5-B639-4E5B-A32F-014956A1194E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8da2e24fdd01894aa0bb79da3299dbde4fd16ce1","datavalue":{"value":{"entity-type":"item","numeric-id":1425190,"id":"Q1425190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$5EF9F39A-F760-49CC-98AE-22115F4CF593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"435bac34a3d647ebababaf5903b7b54b1189ce2b","datavalue":{"value":{"entity-type":"item","numeric-id":1881265,"id":"Q1881265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$2851B993-56EF-4998-8E10-824F790C1602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe7a66982317f943528a01ca680cec7be690c105","datavalue":{"value":{"entity-type":"item","numeric-id":4158997,"id":"Q4158997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$DAC2EA74-DDDD-430D-B826-FC84237E8D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4cd1ee8ddef8c3617a21c4911ab4abb48a578a69","datavalue":{"value":{"entity-type":"item","numeric-id":4808696,"id":"Q4808696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$F9201B2F-B402-45BB-A94A-40688F803315","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$F6F101A1-EEAC-4908-A819-0FBF766D1B21","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$D2451023-1DA5-4423-86FD-8D27CAB6B862","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65292b3c42fa1bd5c21e4c91fe94fdc3f630f232","datavalue":{"value":{"entity-type":"item","numeric-id":7360821,"id":"Q7360821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$A46186F6-A73D-4C05-AA45-EE313D4D28B2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361763$E9A1DB7D-9785-4D81-BAD3-8FD1E5C4EDE3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Kleene Algebra (AFP entry Kleene Algebra)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Kleene_Algebra_(AFP_entry_Kleene_Algebra)"}}}}}