{"entities":{"Q2817943":{"pageid":2828681,"ns":120,"title":"Item:Q2817943","lastrevid":79745789,"modified":"2026-05-06T14:37:05Z","type":"item","id":"Q2817943","labels":{"en":{"language":"en","value":"Machine-checked interpolation theorems for substructural logics using display calculi"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6623279"}},"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":"Q2817943$659ED460-0802-4609-8235-A12F1B0678A0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c22df8702d8f81b11459568c524bc48c4b58e2a","datavalue":{"value":{"text":"Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2817943$A0391607-B580-408A-834E-280FB55B3B12","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa97a8a96396d7921ed8024830c0efa5b85a733c","datavalue":{"value":"1476.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$5F3EFE94-A424-48BE-A93E-89634B2A3D3A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f5087334bdc8eb6eea1582c6cd359597d8ade185","datavalue":{"value":"10.1007/978-3-319-40229-1_31","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$DC1D4443-056E-4DFE-9A21-493EE066DFA4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b218d394a4f78b8be43b552938ed5e21a7cf904e","datavalue":{"value":{"entity-type":"item","numeric-id":1401935,"id":"Q1401935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$2AE33E7F-04B9-46C5-A861-E77E6564C065","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9764b5e3183836adae29ba3fef393bcd0832967e","datavalue":{"value":{"entity-type":"item","numeric-id":229747,"id":"Q229747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$A3E63F2C-BA4E-4AD0-928E-F02F6B72CCBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2459dc77e279bbc9b5ed625e678e226c3ba4ea28","datavalue":{"value":{"entity-type":"item","numeric-id":1051649,"id":"Q1051649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$E5CA0CCD-11AA-421A-8BC9-A58454293973","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$B1640AA5-0FC8-4C0C-AC0E-36D08BB6B516","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c42ad213f9b7f39d3e9ee142840c36c28e5864b9","datavalue":{"value":{"time":"+2016-09-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2817943$C05BB626-CE5C-4F4D-9836-96E8B463FBBF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$65B3A4BB-A0D1-46AC-8C77-06DD45EE177C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$00AB1C58-D0D2-46C6-8330-C9F8458B1F55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$F651D444-5830-471C-A781-0DF3512B5845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$E5F792D0-7AF4-4ADF-84A9-782F6F05ACAF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e52bb00d0d6cc79dd84036f2b30fb0e597e7252c","datavalue":{"value":"6623279","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$A5533A9F-7488-4683-8196-55262927E4C2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03f1ce721ffa5b2f36084f57048f17032077e128","datavalue":{"value":"Craig interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817943$11344D27-E944-406B-BC23-DE63B8768696","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6bc3a19089d3c475a56535a8622363edd5f36cd5","datavalue":{"value":"display logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817943$A1825962-01EE-4C59-A0DB-BEBDDF1F65ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2817943$21AA340C-74FE-4F96-AE9A-45E63075B7B4","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":"Q2817943$11200950-6A8B-4650-BC0D-8D343CBAF965","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":"Q2817943$4FDB2F75-B634-4804-8F3A-54D36A830F88","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1c6762cfd6c00ae308daafb15b5fd207cdebd12b","datavalue":{"value":"https://doi.org/10.1007/978-3-319-40229-1_31","type":"string"},"datatype":"url"},"type":"statement","id":"Q2817943$097B79EF-9FF8-4199-B860-136D7FE1A65E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3976531b7538f773f8caeeba039578025dc60cd3","datavalue":{"value":"W2484729803","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817943$F9227058-3EE5-42C3-872A-3F814BD918FD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b70c7b3f003527069c2310fc828f8afaad5df5d6","datavalue":{"value":{"entity-type":"item","numeric-id":1838471,"id":"Q1838471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$C76CAE60-7B68-4B81-B12D-F73A39C4A43D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1d0ad9d4fbf3812dd470b090823d342931e402a","datavalue":{"value":{"entity-type":"item","numeric-id":3010362,"id":"Q3010362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$0AD93D13-0409-4181-B8C8-F8EF1170EBD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7de140db476e3cb4a77792caeebac28e6bb14357","datavalue":{"value":{"entity-type":"item","numeric-id":3244103,"id":"Q3244103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$CC659529-9163-4075-A6E9-60764FFE3255","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12ca673b668f2b75998f61be11911f94c91cad52","datavalue":{"value":{"entity-type":"item","numeric-id":4484337,"id":"Q4484337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$EAA3F095-2716-43A1-80DA-B1CB1E09E3AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f272d7287f994bc6a285690f7059c71fa20c01","datavalue":{"value":{"entity-type":"item","numeric-id":4933310,"id":"Q4933310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$331F441D-A4D0-4C4B-9CCC-12255C5DB672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd8022da98f09f79b2d52e02a4fd5bb75ea446b0","datavalue":{"value":{"entity-type":"item","numeric-id":1024116,"id":"Q1024116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$3198CEC3-1681-41F6-B46E-031D0BA6D55C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b419bc332d2c3e82611eb2f0ccffc32e0087f3f","datavalue":{"value":{"entity-type":"item","numeric-id":3601798,"id":"Q3601798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$B1603577-A4F2-4BFD-BA1F-16CFD5754A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f1a62c24cddf605dd86a399f231d937d5444e0b","datavalue":{"value":{"entity-type":"item","numeric-id":5458341,"id":"Q5458341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817943$A0BDF139-3321-4152-821E-D0BBF1FCAB53","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e388c54587366ee3fd43103da42eed5f38a1b2e","datavalue":{"value":{"entity-type":"item","numeric-id":3010362,"id":"Q3010362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11f14228089428deb7427655ce1fb0b83bf8c3f1","datavalue":{"value":{"amount":"+0.8434544801712036","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":"Q2817943$8550FFE8-9249-4B70-AE44-18B36E24443B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e15ab56d2932edec5b9ee12d91469df76fa2fb0b","datavalue":{"value":{"entity-type":"item","numeric-id":5505488,"id":"Q5505488"},"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":"Q2817943$D2C06034-6F30-4292-AEA1-5FA8EC33F3AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"446af417b1165c073a34fdc7f7ff570c7db50f05","datavalue":{"value":{"entity-type":"item","numeric-id":2843910,"id":"Q2843910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80b2cd923de6208b5084b122bb8d977967308720","datavalue":{"value":{"amount":"+0.7866261601448059","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":"Q2817943$1D250C7E-D40C-415F-9E6F-F923B1C05D1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d4243d97e0a8017982b8094990ee6233d892c66","datavalue":{"value":{"entity-type":"item","numeric-id":4484337,"id":"Q4484337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04aed3dbb5d546293394329c0f7e1b3973c898c3","datavalue":{"value":{"amount":"+0.7650611996650696","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":"Q2817943$CB6D0CEA-BDED-4A6B-B8B6-7E503B1988CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a2f57ff74cc16c6d2e4cca08d4f026a7fbdc47e","datavalue":{"value":{"entity-type":"item","numeric-id":5702666,"id":"Q5702666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10d5548510a14d807f956e47a420959038f9bf62","datavalue":{"value":{"amount":"+0.7618184685707092","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":"Q2817943$CBF36EDB-3AE0-4D1A-BEC3-F338C2F5B1AA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Machine-checked interpolation theorems for substructural logics using display calculi","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Machine-checked_interpolation_theorems_for_substructural_logics_using_display_calculi"}}}}}