{"entities":{"Q7361028":{"pageid":31518623,"ns":120,"title":"Item:Q7361028","lastrevid":105362447,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361028","labels":{"en":{"language":"en","value":"Kleene Algebras with Domain"}},"descriptions":{"en":{"language":"en","value":"AFP entry KAD"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f0c198031b696b82f0b3f9eb5f328a9908beec8","datavalue":{"value":"https://isa-afp.org/entries/KAD.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361028$EDB77D32-CBC7-4CB3-8AD3-D2B66800AF1E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7b8ac6f04bf26e1f508d280fb4a7b266578e64c8","datavalue":{"value":{"time":"+2016-04-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361028$6837553B-48E8-4740-9F0D-C9993DC80741","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cebadfd7b78bd04e93befe8d7c5151d4488b7f71","datavalue":{"value":"Victor B. F. Gomes","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$3C3D6FD8-40DD-43B0-998C-221DB6F3D26F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3c617235e619eef98fa14e39d518bd5dd86d6a82","datavalue":{"value":"Walter Guttmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$EA333D35-554D-4B5A-B682-4FFDB19AF527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"764f505c166c35794d03c474c0f8d7e266076240","datavalue":{"value":"Peter H\u00f6fner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$0345ED28-6EC6-4C0C-8906-31803D26D707","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"791c9af3f632028a8094f425e13128d157950d83","datavalue":{"value":"Georg Struth","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$5F605375-62ED-4476-8A77-48672E50010B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2f854883aaf7cde2ebd962b9b518c74b730cb624","datavalue":{"value":"Tjark Weber","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$FA461469-2C98-4692-8A33-633CCA1BFDC8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a60b5d928b4568d5be59b323a68151e89311bd3c","datavalue":{"value":{"text":"Kleene Algebras with Domain","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361028$E131B8BC-D0AF-4AEC-9544-FD6E438F7691","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1965af0ca779b02b9e4092bab59fed590ba6f856","datavalue":{"value":"Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361028$8E000FB8-D546-47A1-85C4-7C067DC993D6","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":"Q7361028$A20C5356-C802-48F8-9F11-D036B6D5C87A","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":"Q7361028$88CCC28E-D7BA-4E98-AD94-779478FD66F5","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":"Q7361028$B7A9F022-1140-4802-B775-1ADAC613D3F1","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":"Q7361028$04D29611-FBF3-4BC6-A150-B5753BCDE41A","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":"Q7361028$FA7CB0C9-0914-477D-BD17-44523CFA23BD","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":"Q7361028$F9477215-AD74-4F2E-8748-E5A05FDA2920","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":"Q7361028$031A109F-E4AE-4FF4-AAEA-93DA19ACC7FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45c9d0d67c2f80493f5ff1d22671474150009cb1","datavalue":{"value":{"entity-type":"item","numeric-id":3651509,"id":"Q3651509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$A5308224-C375-4636-B6D1-D58E43DC4473","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":"Q7361028$9568A4A7-922A-4C57-9675-9780F5D8A7BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87c7893913ac74b7ec3bad95e74075ab9512b7bf","datavalue":{"value":{"entity-type":"item","numeric-id":3003302,"id":"Q3003302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$808F1773-CEFA-4A64-B522-9F6E968A6DB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f0dc16508877fecb9994b520f0ed77f4ce3b776","datavalue":{"value":{"entity-type":"item","numeric-id":5505433,"id":"Q5505433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$016DBB34-5A3F-4F94-BAE8-199B8324F854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d5703d8b9ac3f2ec42c5cea3cb6310bb02f051a","datavalue":{"value":{"entity-type":"item","numeric-id":627202,"id":"Q627202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$829CEADF-8B5A-40AD-B651-1F2C8EAA7E57","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":"Q7361028$F3345AC9-0650-4ABE-B7A8-31F36BA9C226","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":"Q7361028$2A24CD4C-FE8D-4F0D-83EC-FC648C324D60","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":"Q7361028$9BD777BD-F3E8-4737-9F70-8042F8E020B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a16cb3de41ef02b5a9305b03bf26fc821592ed4c","datavalue":{"value":{"entity-type":"item","numeric-id":5277895,"id":"Q5277895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$C88EAA21-6F96-469B-8993-18301BD8EE59","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":"Q7361028$E0168BB0-DE01-4DBB-B2FB-D90E91CC1E86","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":"Q7361028$A6981CBB-2772-4DCC-AB54-A4275F921F5C","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":"Q7361028$F5890427-B33B-4B28-9A88-E96DC81087E1","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":"Q7361028$F71EC50A-AFF7-4A6A-B166-82B1C54859AE","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":"Q7361028$93E0E7E8-CDC1-4AE7-BC7C-E07EE52C7A2A","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":"Q7361028$C112314A-A1AF-430A-BB2A-074AC8F6982E","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":"Q7361028$5DA11B60-5F87-433E-9E4B-2D74BDA4BB5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ac0741082eee268d8fb2391d4dc966a1c3f9e9","datavalue":{"value":{"entity-type":"item","numeric-id":868510,"id":"Q868510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$60C9296C-6E52-45B4-A6B7-19569992E207","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":"Q7361028$A06FD986-2F3B-480F-B19F-984025F82DB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62386516d9e4edfd13150a63c443c59cb377920e","datavalue":{"value":{"entity-type":"item","numeric-id":820135,"id":"Q820135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$4499DE08-790B-4A2A-AE12-C21E9EA6FE10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89fd0f9fd1fa7a2df7613d8bd37ed93de45bc31e","datavalue":{"value":{"entity-type":"item","numeric-id":5278188,"id":"Q5278188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$B44BA008-9A3D-4957-8F52-59F29471BB83","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":"Q7361028$1652CFD6-5B47-4199-B4C9-CE9BF8C3AB13","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":"Q7361028$18BEE1EA-BF73-437E-ACC4-37C5B465FD6C","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":"Q7361028$F52BBD40-D8F7-4FA5-BD25-F1CC3393075C","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":"Q7361028$456EFBD7-9413-43B7-BF84-AB2E409D8146","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":"Q7361028$F308B7FD-5568-4DBB-BF52-36E1DAC8C2B2","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":"Q7361028$59DC75EA-FFCE-4417-8CC3-432F594D1EFC","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":"Q7361028$5F913A2C-A3B0-4AF4-8721-B0717B35EABB","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":"Q7361028$0F73E7D1-72D9-4956-803D-CC18D020EFDD","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":"Q7361028$7B25B2C8-0FAE-4AC5-97D2-0F97C0D70A75","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":"Q7361028$8C6FAC83-56DF-4290-B0EB-A02972873870","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":"Q7361028$23372A9F-9E38-4D6C-8CF8-DBCFA76CE8FA","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"b1cb988fa001fdc76ae94cba69a4ea7c1fdb0613","datavalue":{"value":{"entity-type":"item","numeric-id":7361763,"id":"Q7361763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361028$9F70C697-042E-44A2-AB25-447149F50D90","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":"Q7361028$188F244C-F008-4DDC-B650-4116A2830F8A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Kleene Algebras with Domain","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Kleene_Algebras_with_Domain"}}}}}