{"entities":{"Q2871867":{"pageid":2882587,"ns":120,"title":"Item:Q2871867","lastrevid":51900728,"modified":"2026-01-20T12:22:02Z","type":"item","id":"Q2871867","labels":{"en":{"language":"en","value":"Formalising in nominal Isabelle Crary's completeness proof for equivalence checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244443"}},"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":"Q2871867$DE351798-A3E0-4D67-B54C-EA1A28C5F7FD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c381e2ecaaf1650960fb42836c8898ff7f366f38","datavalue":{"value":"1278.68276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871867$3AAD145A-811D-44DC-930E-B7894BE8A381","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7154e8ca53ace223b8c5be019b7f4f775aab0292","datavalue":{"value":{"entity-type":"item","numeric-id":294376,"id":"Q294376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871867$221B8C99-D714-409E-992A-37CBF8068191","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8be13823e57b532010d417bfefa3b5133f759f9a","datavalue":{"value":{"entity-type":"item","numeric-id":860832,"id":"Q860832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871867$DE46506E-7334-48A5-95E7-AAA98F880126","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":"Q2871867$D492374C-F116-4889-863E-DE0A8210DDF7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b35f0f603cfd8bfa38659751dfae9a41765f0c99","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066108000340?np=y","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871867$148963A5-534C-4C05-9E4F-9A3CF49A2B89","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871867$09064A94-9730-4E23-9D99-15B85C75F9F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871867$37398BD0-75C3-4C89-B4A0-7DC762ED9E35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871867$BA99126D-A842-47C8-9FDC-A835458A0854","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"372c2337b880d2e3700493c12b059d46fb3b4b99","datavalue":{"value":"6244443","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871867$2086895E-CC5C-4B89-AF86-EEFC7FA3A4A3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02e2bd1176be2ca24a8b368e42bc8812510b3ef7","datavalue":{"value":"logical relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871867$48088D11-A938-45C9-86F1-DEFE98C6B604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871867$38A2543D-96D9-4880-9990-07FF0669C4C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b1f20c918c912e1b7319416621be9a137eb6098","datavalue":{"value":"formalisations","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871867$47508B0C-3B62-455E-8DC4-AD04329F2A0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871867$A6CB96A6-0BC5-4BE8-86C0-2E9E714FFE65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25e04c1adce31024123171446de348bd4d363a41","datavalue":{"value":"nominal logic work","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871867$6D9E4825-ED5D-4488-B817-4153C4FDD2EF","rank":"normal"}],"P1463":[{"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":"Q2871867$A3C361D8-1CB4-41BC-9351-2791A79BF2AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871867$BCA02587-0AA7-4B66-9850-C3CA6CDD19F6","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":"Q2871867$2EF4FC52-8617-48A9-AC1C-2C04BACB1203","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d9308b8dc3a3c4a1ad2308d964be865ac664f16e","datavalue":{"value":{"text":"Formalising in nominal Isabelle Crary's completeness proof for equivalence checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871867$B0584751-667B-428F-A8D9-0B656149C414","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad70124600704120650b3399879cba7e852de047","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54c62809b1d9ca69bc192acf268c1a878c2118e8","datavalue":{"value":{"amount":"+0.7515089511871338","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":"Q2871867$806A8274-EE70-4A0F-91E2-478BA9F3DD95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a8121b45f5a2121f5d02e937ed3d255985aa611","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7207e91d1ab22bde16ac977e50ff41667fdec18b","datavalue":{"value":{"amount":"+0.7442540526390076","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":"Q2871867$3F0EA87F-4F99-435F-9F37-EF8CD79C7B45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8355bce734d3f9ef7c84b1408dc15c4dd2671ab","datavalue":{"value":{"entity-type":"item","numeric-id":3400637,"id":"Q3400637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a443db8ea01599c2f8c29d1d5fbac973cbfd0f72","datavalue":{"value":{"amount":"+0.7375839352607727","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":"Q2871867$57E3DDEF-5294-4C0E-AD2E-4FB08E139512","rank":"normal"},{"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":"bdadcad52a10ce1284fdb624cbf0a2987e906044","datavalue":{"value":{"amount":"+0.7166841626167297","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":"Q2871867$013A0A03-C327-4EB8-BE96-656FC6ACA2FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"408e6eb37370f869866c0d5e2e591da6ab9b54f4","datavalue":{"value":{"entity-type":"item","numeric-id":3613430,"id":"Q3613430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33b158be763b459b06764a2a41349d7352c218c5","datavalue":{"value":{"amount":"+0.71660315990448","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":"Q2871867$9643A358-27AA-42B2-A6B1-74A92639EBCB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2871867","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2871867"}}}}}