{"entities":{"Q2503400":{"pageid":2514143,"ns":120,"title":"Item:Q2503400","lastrevid":49917532,"modified":"2026-01-12T00:52:10Z","type":"item","id":"Q2503400","labels":{"en":{"language":"en","value":"Computing interpolants in implicational logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5054382"}},"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":"Q2503400$D27668CA-FD96-4318-A711-C9E59C0F241B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6b3e204e31ea23ac44c51699148e8b55d42c6ed1","datavalue":{"value":{"text":"Computing interpolants in implicational logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2503400$D2078574-64AA-4A85-817C-3A06E5B64C91","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c5a06cb57a3f488bcabe03661f4006c77a6cd95","datavalue":{"value":"1103.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$FAF2D4C5-2725-4C61-9361-BB9BCB37CE5E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"20badadc2525610f8a2d3afa834573e622f0289a","datavalue":{"value":{"entity-type":"item","numeric-id":972433,"id":"Q972433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$630683A8-988D-4910-B0A1-0804DD65A476","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$8D7569A2-CBC5-44F3-BA82-AA029A58264C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f4ffc608ada8e4a14c4a7ac75bb9921c404be25","datavalue":{"value":{"time":"+2006-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2503400$F8714340-63A4-4A2E-A7B6-2BFABE3F1C74","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e41aa900af46d0f0023b478289c8213bd4467c90","datavalue":{"value":"Motivated by a problem in the simply typed lambda-calculus which concerns a certain computational model of acquisition of word meanings by children, the author investigates how interpolants are obtained in the implicational fragment of intuitionistic logic. Through a fine proof-theoretical analysis of well-known syntactical methods for proving the interpolation theorem, one on the Gentzen system by Maehara and the other on the natural deduction system by Prawitz, it is shown that Maehara's method gives rise to many interpolants (for a given partition of a provable sequent) including more information than the usually stated ones, but there exist also some interpolants that are not available by the method, while Prawitz's method determines a unique interpolant that is contained in those obtained by Maehara's.   On the basis of this analysis, the author introduces an order between interpolants and provides a new algorithm, applied to normal deductions, which constructs a ``strongest'' interpolant under a certain restricted but reasonable notion of what counts as an ``interpolant''. The argument is carried out by careful use of structural rules, so that the observations are relativised to the substructural subsystems in parallel by suitable modifications.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$95A0EB8E-016F-4481-9720-157FA154768C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$02756B85-D1E3-4624-B27B-4AAD3619F7B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$BF8F27AB-0C7A-4ACA-946D-289D46251AB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$4B6E6E75-0ECA-46E6-8964-599808DF9412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$71AB7E87-054C-411E-BD04-9AA68EFE5211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$ED83371B-C092-4EEB-B4A0-C6BF4F7FF26A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$B69B9794-74B6-4FA4-8D8F-539572B9610E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e58be3509b48086bd5dc758f7358dc913d927977","datavalue":{"value":"5054382","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$4AD9204F-CD0C-4061-8A92-10AF0603AB05","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9bc6474ad8409ef4528af84655741b6b5be3d7c","datavalue":{"value":"interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$CE5FA86B-0B20-423D-961A-833BE84E4721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$08BD54CE-5BE4-43D2-A814-2171F277A10D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7e5d568140a653e809fe0aab6e5f93619204cfe","datavalue":{"value":"Gentzen system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$331D5C04-001E-49C2-B067-9BCB2E9C936B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$93FAE182-7AE6-40C7-9515-FE849A47ADEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"86e893a4a7addf8e22f8e3fcc6df8ecc660c5c40","datavalue":{"value":"simply typed lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$4B4B2B5C-D3F1-425B-86B9-C84655C68118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e19a56a35da34eb08b4ac43272212a5013c8d21","datavalue":{"value":"substructural logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$90206069-8C2C-4110-AE23-11B140C0A3ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d3ed1c17782e31d3d1661abd6299af080ca84f42","datavalue":{"value":"implicational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503400$F0D2AC7B-4A1F-49EA-B111-62373E9F03B7","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":"Q2503400$2FA0578C-FADC-465B-B03B-5FCCDED13880","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3c1a87bcfbb9d9426fbc83ab87e76d52188f54ec","datavalue":{"value":"https://doi.org/10.1016/j.apal.2005.12.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q2503400$66BB42DC-BDCD-4E56-8F91-E2F38C804362","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e67f03bfbdb724782166b2b2f15f3cba58e359d6","datavalue":{"value":"W2086309981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$294C1BC3-3921-4F6C-BC28-9A71D030FC25","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2569f69c28906fddf9d5028580fb85c05208df41","datavalue":{"value":{"entity-type":"item","numeric-id":1304543,"id":"Q1304543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$850995BA-C572-491C-849C-5CFFA0B0E9BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a064c24e33fdb6013bc5a8a7ffdbe6ad695be319","datavalue":{"value":{"entity-type":"item","numeric-id":674415,"id":"Q674415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$D3C87BD9-5E44-43E7-A479-99D303A01E29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38e4f7ab41379ddef17b2784086d259a6264e09b","datavalue":{"value":{"entity-type":"item","numeric-id":1337501,"id":"Q1337501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$DF5A5582-E2C3-4E2B-8303-D4FDE9188EAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85789b0c502cc83f404aecea776e1cd0fe422f32","datavalue":{"value":{"entity-type":"item","numeric-id":4808757,"id":"Q4808757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$5F318A4A-6EC5-41B8-8F19-0767325EA513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$D077A413-7358-474C-918B-AA30791D161D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cad9c94e7533cf9a3a4dbb3d541a81e06befc84a","datavalue":{"value":{"entity-type":"item","numeric-id":1208417,"id":"Q1208417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$1A1EDFD0-DC81-491F-85E8-8785BEA229AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"999c8fe94a19a2d0a1c3cffca1245dbdea8ff1ee","datavalue":{"value":{"entity-type":"item","numeric-id":5736158,"id":"Q5736158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$35ED317F-D873-41BF-BA8F-7D917905772B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"967c49333514bb16993591341675d1365fe80f48","datavalue":{"value":{"entity-type":"item","numeric-id":4397029,"id":"Q4397029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$2520748C-F3A1-4F6A-9823-8DD4FAD817DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05d235b13b6189b04afc72d8494188fd02e92ea7","datavalue":{"value":{"entity-type":"item","numeric-id":2703802,"id":"Q2703802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$15F5833C-9581-4E54-993F-3936A096D6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16a1c588c740fe3cbe85a8b068c195d5be3a6020","datavalue":{"value":{"entity-type":"item","numeric-id":4699355,"id":"Q4699355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$EDCEBEF6-4092-455F-A073-EC04204A8CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4572e78885d1d761d3921cf459ccf6211831645","datavalue":{"value":{"entity-type":"item","numeric-id":4358060,"id":"Q4358060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$7D762C50-8A5D-4732-94B7-D006B423C1F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf5e0864e6808c186dd0092e7f961ddd594b13","datavalue":{"value":{"entity-type":"item","numeric-id":4008745,"id":"Q4008745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$1B2B5320-D9E6-4314-8352-679F94A7E997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$92440AF4-1517-465A-AB49-C3942A2F2ABC","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":"Q2503400$E72B3287-968B-4214-B7F1-86EAFD3627D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f7e9c789fae1e2dace85221a0dc521fd8e520","datavalue":{"value":{"entity-type":"item","numeric-id":3222243,"id":"Q3222243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503400$ED58B497-2758-4305-9BCB-E3FA40A8F66A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8dc4669f9905f4d98585e81de9bc34f5383fc3e1","datavalue":{"value":"10.1016/J.APAL.2005.12.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503400$75411B4C-2155-4CF7-8E5A-D879C0E3CDB5","rank":"normal"}],"P1643":[{"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":"27c4398a46b3b8de579408eeb490837e337acc5c","datavalue":{"value":{"amount":"+0.804356038570404","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":"Q2503400$A01B05FC-DC89-4D38-AEC5-E9A1323E2FA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09ca1e82096cba1e07a69b8ca5d4e2068b28c8fb","datavalue":{"value":{"entity-type":"item","numeric-id":1577480,"id":"Q1577480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef8eb06057f20a6f900b360ae269b144b53d04ef","datavalue":{"value":{"amount":"+0.7875491380691528","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":"Q2503400$8BEEB537-260E-4D69-9F93-283BD5D02128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d63586cbec6a2dc4a917b3c0ae0b568d724bc7a","datavalue":{"value":{"entity-type":"item","numeric-id":3486539,"id":"Q3486539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1fd4fcdb86f649f00321de76b0d2a49a795db253","datavalue":{"value":{"amount":"+0.7761461734771729","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":"Q2503400$CED6A770-FC5D-4E9C-8D3D-9F21ADCD4070","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8c3e74606c40341a9a3c0b7752f33f84cb80541","datavalue":{"value":{"entity-type":"item","numeric-id":4302342,"id":"Q4302342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13bcfb4d191d50c7de958d23ed1e505ecdf20414","datavalue":{"value":{"amount":"+0.7723345160484314","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":"Q2503400$60D31AC5-9C7A-45C8-9281-EF3DC53A4238","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7831872d208bee061f436ff757a77e2205876192","datavalue":{"value":{"entity-type":"item","numeric-id":1130509,"id":"Q1130509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35ead0851266c5d3eebb4b2decac0dc43ad42a71","datavalue":{"value":{"amount":"+0.7667107582092285","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":"Q2503400$2B59A208-8E87-46C9-991A-DE2DDFBD7D8C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2503400","badges":[]}}}}}