{"entities":{"Q777873":{"pageid":779722,"ns":120,"title":"Item:Q777873","lastrevid":64262586,"modified":"2026-04-11T18:41:29Z","type":"item","id":"Q777873","labels":{"en":{"language":"en","value":"Mechanizing bisimulation theorems for relation-changing logics in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7218616"}},"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":"Q777873$C6570292-AB0D-49E1-AF0A-805323034F31","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ca441f6deda7ac3d81c5197ca7ecee76931cbe6d","datavalue":{"value":{"text":"Mechanizing bisimulation theorems for relation-changing logics in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q777873$E1CE6BF4-000E-48E3-A1DA-50B05459933C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d18bfcfc92b497a2065b213b2f24836e4173a587","datavalue":{"value":"1496.03042","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$992A0891-7782-42CC-B810-BF310593A8E0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2070ba0d4a289045f2dd38414f19ca69043e48ad","datavalue":{"value":"10.1007/978-3-030-38808-9_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$1E098CFD-95E2-4B85-B34A-9638C73C2B9E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad060de8da2ecdba9c119fc8db2ca121a0ca8e5d","datavalue":{"value":{"entity-type":"item","numeric-id":777870,"id":"Q777870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q777873$596DF426-B392-41E6-91D6-E021AE806E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2d3c9a7f384e56262db5a91f6c8cd147e674aae9","datavalue":{"value":{"entity-type":"item","numeric-id":777871,"id":"Q777871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q777873$3CAFE5EE-6AD3-4AF6-B950-55C9D0B85CE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"03755d4aabc7831f3051426847269a4a588f5547","datavalue":{"value":{"entity-type":"item","numeric-id":777872,"id":"Q777872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q777873$D26BC100-E918-409B-888C-3D9C1B5F85D1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7a00d12a888ce0ffc3aa72928c7254f31eb87f77","datavalue":{"value":{"time":"+2020-07-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q777873$ABD13D9C-A3FD-4631-9BBF-DD463DAF7DBF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$15F16B33-2637-4F7D-B61E-09BA85D15213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$D2A6C724-EF0D-436E-A5F6-5D807FFE867F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ce859a5072e41f4b353b8b2750eebba46d27d48b","datavalue":{"value":"7218616","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$44B4FBC3-5120-470F-B5EA-CD3410239411","rank":"normal"}],"P1463":[{"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":"Q777873$7632DE8F-6424-4597-A1C8-F69412641951","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":"Q777873$1C9338F6-7AD6-40DE-8A28-01F918ACA122","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a9b5c4f3fd579a6186d3d64d5cfda37f9070102d","datavalue":{"value":"https://doi.org/10.1007/978-3-030-38808-9_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q777873$D911AD24-2CAE-4795-9F0A-04A54BD84D13","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b62b7ccb2e85aef405640692d3dfa00f03cdafcc","datavalue":{"value":"W3000719559","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q777873$47F00737-0212-43A0-B1AD-F526F0DE06B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"150ae9338299f5e5f08685b26bddf8075ea15403","datavalue":{"value":{"entity-type":"item","numeric-id":2035655,"id":"Q2035655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c25a55a60c051257459f14d45a7e10d562b86dfc","datavalue":{"value":{"amount":"+0.9455243349075316","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":"Q777873$B17A0073-9E14-43A9-AC5A-FE81E80A0880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5becc199be0be438307b801ca58515df9c7ca279","datavalue":{"value":{"entity-type":"item","numeric-id":2851950,"id":"Q2851950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7337a31c558b0553684d9058bc2986c8e782ce2","datavalue":{"value":{"amount":"+0.7272939085960388","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":"Q777873$AEDB8284-3225-4468-A7FF-2E689C11EFDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"74907d9756948c4ba03bf28c58939b36b24b0edd","datavalue":{"value":{"entity-type":"item","numeric-id":2643149,"id":"Q2643149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34db3cad56e9948f1bc534704d46a6c6b417fb2b","datavalue":{"value":{"amount":"+0.7121756672859192","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":"Q777873$ADDBFEFD-CDE7-4830-A5A5-EA6D2CA14CA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7aa4c48e9e3153570dbf712f277e18bccc31d457","datavalue":{"value":{"entity-type":"item","numeric-id":4644524,"id":"Q4644524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c952196c5990f9f94ab8561ab80ee9cdbf394943","datavalue":{"value":{"amount":"+0.7057110667228699","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":"Q777873$CABA1D48-637D-41D5-81E2-36FEB1779D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7370d65f5e7cea5c67d03c71f5dc029650ba0e7b","datavalue":{"value":{"entity-type":"item","numeric-id":5015266,"id":"Q5015266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b93c6e737a25579869a1b43dab7da9d9ada8214","datavalue":{"value":{"amount":"+0.6988099217414856","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":"Q777873$DC5F00BD-EB5D-4834-817D-2C9C23C5512D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanizing bisimulation theorems for relation-changing logics in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanizing_bisimulation_theorems_for_relation-changing_logics_in_Coq"}}}}}