{"entities":{"Q2881083":{"pageid":2891803,"ns":120,"title":"Item:Q2881083","lastrevid":51442634,"modified":"2026-01-18T06:29:14Z","type":"item","id":"Q2881083","labels":{"en":{"language":"en","value":"Deciding Kleene algebras in \\texttt{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6021333"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$40B1A50F-6600-4307-A999-89AF4DE0B063","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1ca66813b15994c6ed454654035cde71bc4fc569","datavalue":{"value":"1238.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$EE6EFB70-C155-4F2F-8E38-82729B07A4D4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"df35be840e0fcc7eb1a5f9b5b38a6b146d0a54c0","datavalue":{"value":"10.2168/LMCS-8(1:16)2012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$14F2FE01-68F4-41FA-A3CE-23193736B9F9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"12328682479f4a45e2f0e2c1b6bc2d9e6d8cbf3a","datavalue":{"value":{"entity-type":"item","numeric-id":2351421,"id":"Q2351421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$0F57ED9B-0820-4F98-8331-786C11813845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b609b0474903c90ee98ec931eee072d672864771","datavalue":{"value":{"entity-type":"item","numeric-id":299193,"id":"Q299193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$A8E3AFCA-85F3-410A-822A-FACDCC3633BB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$6BADDE2C-4CF1-4B48-AB48-52D572C3E610","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d567b51f320d6b206f1e246178a080db047a3948","datavalue":{"value":{"time":"+2012-04-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2881083$96896437-10B0-4513-A2E8-C01F0260C7F2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$298328AE-3558-4DA4-8D54-49792CF4B34B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$F4A20462-151B-4C94-A545-E8061D94DC2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"deb5f9f43f355c6575c467b17adc4a680e013b41","datavalue":{"value":"68Q70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$D884C3D5-0593-4F7D-B763-2A287F066963","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c364aa8edc29aefb903343bf65cfa3abfec6348e","datavalue":{"value":"6021333","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881083$4C311957-D731-44BC-B974-F3DF26A755B1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5dce58886ffc63b5facc93c53510fce5628bb35f","datavalue":{"value":"Kleene algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$D44A4855-98D0-45E4-8E55-8126F2E695A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb8d04c869a7c957a2fb637bf61f6c6b39fe9a39","datavalue":{"value":"regular expressions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$3C339ADB-DE67-48DB-BC0B-A1CFACFE4706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$F140B71C-DACA-406A-99BF-72B14FC58C15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50070997a3eb672eae615ed68215d674ea65d5f8","datavalue":{"value":"\\texttt{Coq} proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$89520C8F-DE62-44C6-8727-B6B9760DA97C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a15950c97c72cc9a6f99bb0365abc69e54818ea","datavalue":{"value":"reflexive tactic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$4953E4A1-A400-4951-A699-1D7D12679EEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8fe1ec072eddb82e8c6723b370c91fea5db0efe","datavalue":{"value":"finite automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$08821B7B-64FB-4B89-9B1D-763F97E753A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0912ca4b29be2e77907d20f34cbe52ae2ffa70c5","datavalue":{"value":"typeclasses","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881083$9B4D44F1-6FFF-43CA-B13B-07F5F97810B6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e916eb1dc395e3830d6317d3e8aefcb052d11440","datavalue":{"value":{"entity-type":"item","numeric-id":21785,"id":"Q21785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$74C6D4E9-6F89-465E-BE33-318C6206A16A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$B01C4301-372A-4726-BEE5-D5A0FAA9120E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d0b3613afdea99b20a3156b582c84af8424d5eba","datavalue":{"value":{"entity-type":"item","numeric-id":20514,"id":"Q20514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$E2489204-89B6-4840-9204-A8ACE44549E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3fa29bf2151fbe16d38e398c515ac9a9dd0ab16c","datavalue":{"value":{"entity-type":"item","numeric-id":40507,"id":"Q40507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$F02BCF87-370B-4F24-A951-C60BDFD84F35","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881083$95AF86A6-00E1-4904-B0D8-0F3D0DFC46DC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b54aede307fe783c4b9b5f62b7cc25e508539847","datavalue":{"value":{"text":"Deciding Kleene algebras in \\texttt{Coq}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2881083$C707C30B-A0AB-4819-95B6-FDE5D88BD1A8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"793d268335cb0310030c003f9a67cbb04ebc75e9","datavalue":{"value":{"entity-type":"item","numeric-id":5747648,"id":"Q5747648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7fffd251ea83f8d490c8dbb127fc97b6679d8a9a","datavalue":{"value":{"amount":"+0.967350423336029","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2881083$17FA255A-7DF8-4C70-B20B-B7F06611ED20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e185cb3788129a86496b6b33cbf65d270bfb21f","datavalue":{"value":{"entity-type":"item","numeric-id":5327344,"id":"Q5327344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdd5501f829b92384a8da97137bb6f2c6d991deb","datavalue":{"value":{"amount":"+0.8241574168205261","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2881083$E30FA963-1090-4DB7-94F2-A76584A948A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d9e196f571c37d4132741b2b78c61cc2cbd633e","datavalue":{"value":{"entity-type":"item","numeric-id":2347910,"id":"Q2347910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a461331ad2bbe32cb35504d16e6324efda9202f6","datavalue":{"value":{"amount":"+0.8113783597946167","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2881083$AF06321F-E6E8-4151-AEC7-91C9A8AC4DE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d5eef8b48d283545bb773ea2f0d3ccc1e01255c","datavalue":{"value":{"entity-type":"item","numeric-id":3073622,"id":"Q3073622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"297dcfe86edcb8dedd1e04ec082ea50a4b5f1700","datavalue":{"value":{"amount":"+0.771114706993103","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2881083$0AD1ADE5-ABFD-4D34-B077-A4969EC84C14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2337f63657bead5b56d0f24eceaf33426fdbcf75","datavalue":{"value":{"entity-type":"item","numeric-id":3299849,"id":"Q3299849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26af4778370b895098033533b1447813b2c9462b","datavalue":{"value":{"amount":"+0.770305871963501","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2881083$E85A6AC2-76DE-4C16-A60A-1B7AA40D52C5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2881083","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2881083"}}}}}