{"entities":{"Q1006613":{"pageid":1008461,"ns":120,"title":"Item:Q1006613","lastrevid":50614640,"modified":"2026-01-14T14:05:36Z","type":"item","id":"Q1006613","labels":{"en":{"language":"en","value":"On lengths of proofs in non-classical logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5532839"}},"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":"Q1006613$2E166616-7821-4248-A54A-354F476AEBE4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d3959aa6dcd336fbdce92d01b147260a706b5b3d","datavalue":{"value":{"text":"On lengths of proofs in non-classical logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1006613$1BEBBAE7-EFCC-4E68-90AA-4C5A9EE6705E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ad05116cb8eecdd35c99302270ac5aa178df923","datavalue":{"value":"1161.03033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$A5D190DE-9D92-4BAA-9918-5F757317F420","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e7ea3ca54733938686f141270931e22fee1769f","datavalue":{"value":{"entity-type":"item","numeric-id":436565,"id":"Q436565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$0639119F-7D93-434F-944D-E4534E518079","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":"Q1006613$58CBF40F-108E-49F5-857D-FD5C0DD24C72","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f17d548f42efb27321ed2d9ca45a732b10fcb2c","datavalue":{"value":{"time":"+2009-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1006613$F4E5364F-16D9-4D0D-BC57-E227CFEE2940","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"957b907f6cd91860573baf9f785e7e74d75ec872","datavalue":{"value":"In a pair of recent papers [J. Symb. Log. 72, No. 3, 941--958 (2007; Zbl 1125.03043)], [Ann. Pure Appl. Logic 146, No.~1, 72--90 (2007; Zbl 1115.03081)], the author proved a version of the feasible monotone interpolation property for some propositional proof systems of modal logic and intuitionistic logic, which implies an exponential lower bound for the systems in question. The original proof relied on a complicated model-theoretic construction. In the present paper, the author gives a considerably simpler proof of a more general feasible monotone interpolation theorem for K and intuitionistic logic, using a representation of modal axioms and rules by Horn clauses. The result implies exponential lower bounds on both the number of distributivity axioms and the number of necessitation rules in proofs of variants of the clique-coloring tautologies.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006613$7F9DA08D-4A96-4BE0-9F2B-EAF63F4967BE","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$26BEFA6A-EEA4-4C0E-97BA-8B7788068D95","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$9CE2C29F-A3DD-4709-B33F-BE0CD0B8F1BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$6A59D4CF-5405-488C-AB2F-5811D82C3C51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$23FBA696-2796-45DE-9EEF-F02E94052073","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"64619dd42dc71b5a50a8c60bafaea1716b825c66","datavalue":{"value":"5532839","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$537793F4-6795-493F-8D2C-86AE6DDE05BB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"beacc345177607df4ab1f59f0170626c9d1a1d90","datavalue":{"value":"propositional proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006613$F07BE3BC-5416-48DA-AEFC-DDF0A583AFAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"72f1b47ff68adf8abb83839bd6f1bd41ad4f1806","datavalue":{"value":"feasible interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006613$4A3691AE-3A90-4DFC-A79E-37258B63B34B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006613$894BEF75-DD2E-45E8-9979-1E236668427A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006613$D0B54248-28B6-4EAC-BAD6-AD6528C8A110","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":"Q1006613$635826A1-53BD-47EC-AAD3-F3A70C4B0AA4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e529366719a391488a7cbb38d116be272241f922","datavalue":{"value":"https://doi.org/10.1016/j.apal.2008.09.013","type":"string"},"datatype":"url"},"type":"statement","id":"Q1006613$1793A3DD-245D-4044-9D8B-52EF94A1DFDF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"668926dfb377658f99a4f51bb6bd97049181ac11","datavalue":{"value":"W2012102524","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$23DAE1FA-61E7-43D0-858C-FFDBAF0D1D7A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2ca04c59b1468ff9eb03a30febcf55d98359908","datavalue":{"value":{"entity-type":"item","numeric-id":1094870,"id":"Q1094870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$078C6B84-B420-4F6B-B413-4EBB7104D76E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41cfc6d1ca649e77a169b6cd08a9283c8c165615","datavalue":{"value":{"entity-type":"item","numeric-id":1304542,"id":"Q1304542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$8941E2F1-A84F-4E3D-9A9A-56C1F5CDF3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aadb89586b12baabd090fee59e578386a236b4eb","datavalue":{"value":{"entity-type":"item","numeric-id":5422311,"id":"Q5422311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$79C1F23D-8CA8-433D-9C0E-F33302B789E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aff4ee6a73fbacbcf6d7da620a82d0b3fbe596a6","datavalue":{"value":{"entity-type":"item","numeric-id":876385,"id":"Q876385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$807DCBCD-BF19-4D3E-8CBD-BB0781C17907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ea72334575ec9f68c192adc857ab078ff1e97f3","datavalue":{"value":{"entity-type":"item","numeric-id":2503409,"id":"Q2503409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$53B8C88A-BEB3-44D8-9147-6C92E3B66BB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0942c3ffeac8339c20eccc6667aba9b8af08cc5f","datavalue":{"value":{"entity-type":"item","numeric-id":3758729,"id":"Q3758729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006613$4E742920-C117-452B-90C8-F1A93967630D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5eed7b225803f565ebbfdf5ee60dfcedd05fa451","datavalue":{"value":"10.1016/J.APAL.2008.09.013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006613$D22F5B0B-0D7B-429C-8664-C01355C8832B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98dc4b7ceef9e5ff2113f203b50f7b4436628f05","datavalue":{"value":{"entity-type":"item","numeric-id":5422311,"id":"Q5422311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d12610f290346cda505a0b841b9182de436b0c67","datavalue":{"value":{"amount":"+0.8352582454681396","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":"Q1006613$6B47BE2A-C12E-42A0-AC55-9487C931BDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1269c00f0711ecb81cbf4aad4a737f26c703bf9","datavalue":{"value":{"entity-type":"item","numeric-id":876385,"id":"Q876385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15af5324d0f1a6a93be3e33e811404cfe7ce37d4","datavalue":{"value":{"amount":"+0.8290627598762512","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":"Q1006613$393F864E-6E39-4D30-AF4D-5CF5BE6D9539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d35a882d95def01bb1e340945d093cd4b5396128","datavalue":{"value":{"entity-type":"item","numeric-id":5100154,"id":"Q5100154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5ddb41a67395c2cf4d686b3bd278fa9ee3aff52","datavalue":{"value":{"amount":"+0.8201163411140442","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":"Q1006613$B642F6B3-EBB2-4AAE-8937-C6D144033E04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02e55b61410f38e6a1b24aaa79cfee91f308ed35","datavalue":{"value":{"entity-type":"item","numeric-id":4934563,"id":"Q4934563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85b9a98ea12873fd9f6442a0796183779f7d91eb","datavalue":{"value":{"amount":"+0.8034269213676453","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":"Q1006613$61EC3C75-3FFE-4B8B-A7AD-776739669A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cd8a30ceea8c23c439b0c2bf57e1776b9f2d4e0","datavalue":{"value":{"entity-type":"item","numeric-id":4358049,"id":"Q4358049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85b9a98ea12873fd9f6442a0796183779f7d91eb","datavalue":{"value":{"amount":"+0.8034269213676453","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":"Q1006613$64A81F8E-DBDC-4F8D-9472-C4958685A57B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1006613","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1006613"}}}}}