{"entities":{"Q5505488":{"pageid":7535048,"ns":120,"title":"Item:Q5505488","lastrevid":50550227,"modified":"2026-01-14T09:03:54Z","type":"item","id":"Q5505488","labels":{"en":{"language":"en","value":"Mechanising a Proof of Craig\u2019s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5498215"}},"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":"Q5505488$123A0615-3AC8-4CF6-A377-B9177E9AC45F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8302ecdbdf3f8e5cf2a515e92ba01f22016e6f2b","datavalue":{"value":{"text":"Mechanising a Proof of Craig\u2019s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5505488$9946FE32-690F-4A27-979D-B18E8E51D7F5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"881c270e4ff046952b855bacd147760838f595cf","datavalue":{"value":"1166.68340","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$1D741663-73B5-42B6-BC6F-96074C823C9E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"115d20547db9af3e6113300ec3134d2252a12770","datavalue":{"value":"10.1007/978-3-540-85110-3_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$7DE7F624-61EC-477D-83D2-A0FC59064234","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa25152ae20713759607233b76c961131f0f0a7a","datavalue":{"value":{"entity-type":"item","numeric-id":2029593,"id":"Q2029593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$1B407D41-586B-4391-B5FC-163E73B5F9B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6d72c052d6a5ad7a719f388761353f23640a4e3","datavalue":{"value":{"entity-type":"item","numeric-id":1725925,"id":"Q1725925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$9333A2E8-4938-49E2-9703-FC1DBC767020","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":"Q5505488$2C98A14F-C080-4A3F-91F3-BC7D5042C27E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$3A1A3F8F-0B47-4C61-B4AC-68FD4A9B18D9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"51e6c39ac6ec91b8381a06fe1e16cf5aca0f2bdc","datavalue":{"value":{"time":"+2009-01-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5505488$88552C79-A733-433B-9906-32E9F9A800E7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$934F8AC3-7678-4C8F-9C30-DD441FD713C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$2B9D70B4-5275-4D41-AA44-7D32784772BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$AB17BD98-F310-4D69-AADE-1A71A4117DC9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f1bb6775fb1c1ac07d82f3fd94ca6503a1f6f57","datavalue":{"value":"5498215","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$77F1AEE7-3798-4018-8916-6453BCA19885","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc238ea6cb52c715bab39832f2cd5b4837c9294f","datavalue":{"value":"formal mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505488$5CD6EA8F-BDC3-457D-B673-9AFB492E68AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b94cf12b514b82bd9372646d7199e845de3b7b90","datavalue":{"value":"nominal Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505488$82023E86-0EC5-485E-882A-3F1F173A97F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505488$90A76426-3BF6-4479-8100-6975BA8682CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4bbb0c1d4a0dde26226934f7234d049627289106","datavalue":{"value":"logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505488$55B60BAB-8ABB-4778-BCD2-07977B8C1048","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":"Q5505488$1D7105C8-C4C9-48F4-A758-A7760BBE9C68","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":"Q5505488$BB6C5999-7229-4BCE-8F1A-BE838FDD5064","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":"Q5505488$53FBFC7C-277A-40B6-945A-0FC7B3208FA9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eeb1f9d74cbdcd28276947e635f6285c85440611","datavalue":{"value":"https://doi.org/10.1007/978-3-540-85110-3_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q5505488$90D005B2-E3F4-4CA1-B1F1-5A49DA0A8BC4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fbb0c31c59d1062f66248f7d149a7c53f6ff8bbc","datavalue":{"value":"W2098316338","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505488$0D3FD334-6B7C-4875-9A5D-281C45C74B66","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"59952b81e0c5561a3960659f42a8c0f87be78073","datavalue":{"value":{"entity-type":"item","numeric-id":5758131,"id":"Q5758131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$67386F71-3996-4150-8A2C-856DED52ADEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"347ff5e243a44fe280b61636b43f4d0e72b66679","datavalue":{"value":{"entity-type":"item","numeric-id":4281480,"id":"Q4281480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$937DD2A0-A56E-408E-A12F-552C4BE2701D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f54bc0e2f92beb50e9c6902664de23aa76daffd","datavalue":{"value":{"entity-type":"item","numeric-id":5703754,"id":"Q5703754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$446454DD-0096-4342-A577-36A01B20031B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8219577a178b5e6bc0cc5aede73996c94784449","datavalue":{"value":{"entity-type":"item","numeric-id":4435474,"id":"Q4435474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$CCB3E32E-7193-4260-8434-3CCF59A63345","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9dd741c8f779448cca2e557d9c65f69f1eb3195f","datavalue":{"value":{"entity-type":"item","numeric-id":1854335,"id":"Q1854335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$5CB131E6-299F-4822-B9A8-AA89500A138F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3652d520789475601e366029ce7b257ab62a1ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5905909,"id":"Q5905909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$A49E9D2D-7A5C-426B-B4C4-20968D35D0C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f8f6dff394ac274489a2a8165abb84f760b4be","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$67DC207F-820B-46A9-9E15-5F472FE1352E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505488$99E516E8-AD56-40A5-9BC3-B9DD5EAB0A67","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"078f018651441429470a4eb1ca473484a825cacc","datavalue":{"value":{"entity-type":"item","numeric-id":2817943,"id":"Q2817943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d14955a94bdd8b6109edbc2c1bf6ba840c9820de","datavalue":{"value":{"amount":"+0.8079577088356018","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":"Q5505488$A381529A-A194-4F27-A2D7-B0189179D1D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75202bb163f4cb75901808c3f92f40ba813a22fb","datavalue":{"value":{"entity-type":"item","numeric-id":1906666,"id":"Q1906666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4be48c18169dbdc032db3bb314e2fc34911ccc42","datavalue":{"value":{"amount":"+0.7929137349128723","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":"Q5505488$281F4D5F-593F-487B-B391-46166C1125E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ee5995a8d18938cd4f7f91e17c063036b95f598","datavalue":{"value":{"entity-type":"item","numeric-id":1821770,"id":"Q1821770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"024aaa6e81ae110b02d91a38bf06389c0cf59260","datavalue":{"value":{"amount":"+0.7927592396736145","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":"Q5505488$5A7ADB03-7884-40C1-A799-4C6A8AD05BF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"660b225cd944f498669ce74a3881521b2f2a3caf","datavalue":{"value":{"entity-type":"item","numeric-id":1876090,"id":"Q1876090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42cdddb387ffeaa618170c87db272647c3d5ca3a","datavalue":{"value":{"amount":"+0.7879652380943298","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":"Q5505488$687462FB-D562-4B15-90A6-702D3136A09F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78829c21b4f9e3193e0fa304034a7fab0cd1144c","datavalue":{"value":{"entity-type":"item","numeric-id":1006639,"id":"Q1006639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7a27393771603b14aee37bfaa6aea7953a2abf1","datavalue":{"value":{"amount":"+0.768083930015564","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":"Q5505488$466FEE78-CC8F-4BFB-A3CD-9A3E84A44D83","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5505488","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5505488"}}}}}