{"entities":{"Q2871830":{"pageid":2882550,"ns":120,"title":"Item:Q2871830","lastrevid":79529798,"modified":"2026-05-06T14:07:44Z","type":"item","id":"Q2871830","labels":{"en":{"language":"en","value":"A completeness proof for bisimulation in the pi-calculus using Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244359"}},"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":"Q2871830$3A3FCF9D-7DFD-4B45-BF01-2E6A25B5D569","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7c8c4be5c314a900e6fc6cad0e0ab7858ebb4406","datavalue":{"value":"1278.68212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$76B5E12B-D2A2-476E-AA55-292B70F652FA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4016e1f23463ca2cfa7c5bb34d7ce64f66d3ab32","datavalue":{"value":{"entity-type":"item","numeric-id":287320,"id":"Q287320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$5E3ECF7F-0863-4C90-BED3-CE0CF9C0D76D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"80e958f9a9f32007b96d202defeeabd37a16004f","datavalue":{"value":{"entity-type":"item","numeric-id":287321,"id":"Q287321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$3BEBED7B-1116-416C-B3A5-8CFF6CFB0305","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$1374FB12-EE7A-4C3F-9122-3C10DCE6C784","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c704b287c68a3d4d8361a025642d6eba13574eb","datavalue":{"value":{"time":"+2014-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2871830$8785DBA5-5B0E-475F-9907-DB25CB2A3117","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$5E2E27EA-2122-4254-96C6-A7F37E35D1B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$A3BFA879-C28E-4425-A44B-1ECB4029D2D9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b2a1315383f2bc5999b9ccccb775772de9bc0d2d","datavalue":{"value":"6244359","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$DCB97FA2-0CCE-400C-BD9C-178CC211BC38","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e5cedc1a875d8083748dd695c5b423bf932b1222","datavalue":{"value":"pi-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871830$EC2916D9-3E41-4B91-8E78-067EA6D01ADE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b36661f0a3390102be2be05796702400601b738","datavalue":{"value":"theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871830$5B72BE3A-F967-475D-B411-C3A00F85964E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871830$A7797EE0-6E10-48C6-A4CB-7A963EB99AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3e04a2b734a1cac93a9ddfefc5a4de51edbfaf1","datavalue":{"value":"bisimulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871830$E54084A2-0194-4949-AF8A-AB5959B11648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c4978f2c4d263ef258ed0ffc576a325d510c4d8","datavalue":{"value":"axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871830$B6F285EB-3183-49D3-9F80-8D7874A35BE7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$1B7A6A04-B035-4271-BDD1-B600AD75BA4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$3FAF4685-687D-4656-8BF4-6B5A548C02EC","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":"Q2871830$7BCC31E9-AD5F-4CF3-B004-044C1067A24B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5835ee7107a2ca0d8bb2c29f481eae82c863ebb1","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2007.08.017","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871830$D53F4213-FC31-497A-96B6-6A8BA90F3DCB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"911a3e81859d6b05792ff4805b074dc8cff8fc9f","datavalue":{"value":"W1967451324","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$158DC4C4-87FD-4BC9-8BCB-6DD726D85B59","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce39ca711bf99c74f8bdce078c27fed133ff4aa7","datavalue":{"value":{"entity-type":"item","numeric-id":5758048,"id":"Q5758048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$B993244D-AFFD-424A-8070-5D5F52E2C50A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a5b239a2f303b2c8313b2ef3a973a6390b54360","datavalue":{"value":{"entity-type":"item","numeric-id":4664925,"id":"Q4664925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$3B7494CC-D8BA-4B0C-8929-348912EBC286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf8ebc11e5152a7aaca233f3b6037de5f36fc738","datavalue":{"value":{"entity-type":"item","numeric-id":3766826,"id":"Q3766826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$CCD91870-F33A-4F1B-A002-E8E34879E9AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4db8f7fa996304ee694716b3fc5e63d2e83c95b","datavalue":{"value":{"entity-type":"item","numeric-id":4365103,"id":"Q4365103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$152F34F6-062C-435C-A082-49407BF0FFAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bce890db8f764308dc9d80705e866747b01fc19","datavalue":{"value":{"entity-type":"item","numeric-id":1589654,"id":"Q1589654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$94655BF6-0270-47BB-989D-F3DFFEBEC890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a75734f1eb76fa3951a16a34a4963235e3f72784","datavalue":{"value":{"entity-type":"item","numeric-id":1198549,"id":"Q1198549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$C3D482F3-E1DB-4C1D-8375-958F97CA3F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$CA6604F0-B2F4-4DEE-BD1E-3901B8D1030D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9dc2f7f952092927dacd0d7a73c8568f10e239b8","datavalue":{"value":{"entity-type":"item","numeric-id":2760245,"id":"Q2760245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$112555FF-4E2A-467B-891F-BB805FF5AD43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85027313a201258674ff07e8ac17dcd6d794e399","datavalue":{"value":{"entity-type":"item","numeric-id":4457837,"id":"Q4457837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$8688E2CA-6384-4AD9-9B74-C32929DB5376","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f1a85252a4c0a5bb2b7a3eae3c76b6088496bd","datavalue":{"value":{"entity-type":"item","numeric-id":4296962,"id":"Q4296962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871830$4CCD9F67-B049-4532-A622-DFD4730C5E9E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"29185e1ad51d38720241f7d8b52202ea12dc18e3","datavalue":{"value":"10.1016/J.ENTCS.2007.08.017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871830$5E883680-7447-4EB7-A9F2-119FBD8395D7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a9149a6befe14a0285cfa372f007fce8bb115231","datavalue":{"value":{"text":"A completeness proof for bisimulation in the pi-calculus using Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871830$088347A1-9EB5-4DD1-84D5-E4351E0A8C64","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0404f6afbb7eec6187725b2ac097aaa6232258b4","datavalue":{"value":{"entity-type":"item","numeric-id":3395094,"id":"Q3395094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f497caa91784417f07ddd23b2391269dd906d203","datavalue":{"value":{"amount":"+0.8290247917175293","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":"Q2871830$B180ADEB-395D-4ED0-BD8B-F228E69EE570","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fb48cb7bedc08c9ea202a315d981bb139155841","datavalue":{"value":{"entity-type":"item","numeric-id":5758048,"id":"Q5758048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31cf8fcb539c7c3add1b2ecfde05ac0b6209100e","datavalue":{"value":{"amount":"+0.8244903087615967","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":"Q2871830$E4BD9790-00D2-45DA-A0B6-65291E9F0DC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92814dd190447dc3809529a7c8a0548de19c5bdd","datavalue":{"value":{"entity-type":"item","numeric-id":3024855,"id":"Q3024855"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"049e622e3576ffea0f147128b9761faa707b8594","datavalue":{"value":{"amount":"+0.7898925542831421","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":"Q2871830$AB1D5EAC-D7DD-467F-B7C8-251F20FD52E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07490e1bce39583a5e0e8b2142a40bbd51002c14","datavalue":{"value":{"entity-type":"item","numeric-id":5096731,"id":"Q5096731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ba264015537be147fb2785ca41c1b2bc263cf01","datavalue":{"value":{"amount":"+0.7723603844642639","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":"Q2871830$C078860C-7E91-4261-9BEA-B364A33EDE55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"877e985b3380fe71465aa52cef28be711fc2e9a2","datavalue":{"value":{"entity-type":"item","numeric-id":4365103,"id":"Q4365103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e02aadacaf36f267904bfc69d139c2cc031d064","datavalue":{"value":{"amount":"+0.7713496685028076","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":"Q2871830$817079F2-19D1-4B86-B701-98637589C036","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A completeness proof for bisimulation in the pi-calculus using Isabelle","badges":[]}}}}}