{"entities":{"Q876385":{"pageid":878233,"ns":120,"title":"Item:Q876385","lastrevid":50074894,"modified":"2026-01-12T21:16:53Z","type":"item","id":"Q876385","labels":{"en":{"language":"en","value":"A lower bound for intuitionistic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5144417"}},"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":"Q876385$6C2B4FB1-B099-466C-A63F-E6F3B9FD9882","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"34fd875b9513a1671213413f18c95dfa4463fe14","datavalue":{"value":{"text":"A lower bound for intuitionistic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q876385$C727CD10-4B66-4D95-9BF9-31501D52D25C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bfdcf15ed820a2ad2eaa043234d498f9ad13506b","datavalue":{"value":"1115.03081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$C8FDAEFD-2D8E-4781-BFA1-488D96CEC4BC","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":"Q876385$BC308F6C-6581-4211-8684-3D0E5C9C2B94","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":"Q876385$4357721B-06AD-4FB4-8086-EB34DA79A3C4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6f339c49c589764265da0f7de34a17b3e7a78e06","datavalue":{"value":{"time":"+2007-04-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q876385$44BAEEF0-215E-4084-9C17-5A3253F41A88","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"dd32c06b33d9103b7d85bde5ff442dd584ac670d","datavalue":{"value":"The paper proves unconditional exponential lower bounds on the number of proof lines in the Frege system for intuitionistic propositional logic, which solves an outstanding open problem in propositional proof complexity. The main tool is a variant of feasible monotone interpolation for the intuitionistic Frege system, which is proved using a translation to the modal logic K, and a modification of a monotone interpolation theorem for K given earlier by the author [``Lower bounds for modal logics'', J. Symb. Log. (2007), to appear]. This monotone interpolation is then applied to give two examples of hard intuitionistic tautologies. It is also shown that these tautologies have polynomial-size classical Frege proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q876385$C86069E2-B628-4F57-AA6E-9027E17EF43C","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":"Q876385$12EC1142-D5A6-4B6C-80B0-99BBB3823C08","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$4CB41D0D-42D8-49D4-9B60-81E8A25C3B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"87f66489f0c14f30094b654591a05fdd61321103","datavalue":{"value":"03B55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$62D54111-0912-4849-9DA2-4574537A14E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$C9A7EC1D-70C5-4904-AE7E-6D31F5EFA2B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$AD9269D9-90BC-46BF-B8D6-7776CB70F4E1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6464c4784414b6c3e22c45e5569a5ebff444b3a1","datavalue":{"value":"5144417","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$10D2F48D-577D-4153-8249-DD34B053478F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q876385$6603E0E9-A06A-4376-BAAF-7EF55410EA95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q876385$124C1B06-1026-45BF-AEFE-AB61DF6E68E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q876385$D9EEA065-A2B2-4CA3-913B-F84E1DC29E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b8cb70894e2a9655efdcbcc7408847d5fa4f57c","datavalue":{"value":"Frege system","type":"string"},"datatype":"string"},"type":"statement","id":"Q876385$7A4DF7C5-E013-439E-A7E5-ECABF01B2F42","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":"Q876385$9DA78EB7-B58A-4F83-8485-C4A0CBBD3778","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"30ebde58e747160983063e597a7221c7ed1da65f","datavalue":{"value":"https://doi.org/10.1016/j.apal.2007.01.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q876385$B896A13A-E6F6-4504-A967-8D463FAAADD2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7b4ace98e8943cd9e984393523527ba70448d252","datavalue":{"value":"W2017209655","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$03D372EC-53A9-47D4-88AC-00138084DB2E","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":"Q876385$24E8E328-15F0-4393-B326-BF48FCEAB025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f31cbeafb74eb2331031a6d2305fa02411af3e7","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$25238BAC-E53B-461D-9E03-2F6920D347DE","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":"Q876385$2AA989B0-F23B-4262-964D-6C7F18DFF859","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca8e2226bc49403f5d34bedd57297744e386790","datavalue":{"value":{"entity-type":"item","numeric-id":1168215,"id":"Q1168215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$5177611F-6792-4190-AD37-6F78EA6D4AE5","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":"Q876385$1367BF47-F3CD-4D30-9B17-EFD1F1469675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30b9e272f8ccce6a7b10c8e4afc506dcafb4f348","datavalue":{"value":{"entity-type":"item","numeric-id":4358049,"id":"Q4358049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$DB15C19D-969F-489A-9AB8-021411A623F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f9864cd692e177ef3a771b6df84de7a4d93d51b","datavalue":{"value":{"entity-type":"item","numeric-id":5460922,"id":"Q5460922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$FB7A6EDD-2A46-4378-87B6-E1D3653B36A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f45d398cee7029b6c4eb7c6c0e2a1a407fff02c","datavalue":{"value":{"entity-type":"item","numeric-id":4934563,"id":"Q4934563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$EC9192FB-1309-481F-B15B-D22F1CC5D441","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":"Q876385$67BAB932-676C-4F1B-AECB-99E17BBF67D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cea085d8c059c5f81ccc8c6d0a2a9f9fb30e1313","datavalue":{"value":{"entity-type":"item","numeric-id":1259589,"id":"Q1259589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$EE4E8F52-5AF8-49A1-9E56-E93810E194CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97f4c503de285dc0c301d05309603aa1fd461cdc","datavalue":{"value":{"entity-type":"item","numeric-id":3922672,"id":"Q3922672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$84B10E06-1FE0-4327-AC39-00F677355F95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b2e8fdbd72d4413672bdc0a2c0dcc9057a5f41e","datavalue":{"value":{"entity-type":"item","numeric-id":1813126,"id":"Q1813126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876385$74374BD5-D541-4F80-B369-0B1C15470C99","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1ed7935fc40a1490e64ab2247ea4fa5478737016","datavalue":{"value":"10.1016/J.APAL.2007.01.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876385$64739770-5AC0-404E-B29B-3D0F80C7D3BF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6ec113b23214e288da260f9f7085565692b35cb","datavalue":{"value":{"entity-type":"item","numeric-id":1006613,"id":"Q1006613"},"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":"Q876385$4B52C009-7ABF-48C3-B800-476EFC526284","rank":"normal"},{"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":"2495ccfa946c6949fd7183694cd8c7126b29f759","datavalue":{"value":{"amount":"+0.8057249784469604","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":"Q876385$0C940FC0-9016-4FEE-9C83-7533E5FAE117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1fb3f97197cc5507bdb6e9313478f714e3311063","datavalue":{"value":{"entity-type":"item","numeric-id":1204120,"id":"Q1204120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7c9af2aa8efa82d7960a893ef8bd19410df8229","datavalue":{"value":{"amount":"+0.7866600751876831","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":"Q876385$49D5A6F7-1E2C-4EB5-9A62-8A4E6CE408A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4e3bfa89bbce593c83c8f2ca50e1fbe1bc8b7d1","datavalue":{"value":{"entity-type":"item","numeric-id":2032997,"id":"Q2032997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04c7c30344f004e416034ef217ce1589ece0d3ce","datavalue":{"value":{"amount":"+0.7859311699867249","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":"Q876385$C8D56F1E-749F-4C1A-8071-0E96F5E830A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ffa2d7418e931eb671fcf01954fd4a349e35ca8","datavalue":{"value":{"entity-type":"item","numeric-id":2826389,"id":"Q2826389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5b10d16700109526c36cced2b14626c0f14c39a","datavalue":{"value":{"amount":"+0.7848098874092102","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":"Q876385$E59B5164-DE64-4061-9CB3-78B3CF875F80","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:876385","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:876385"}}}}}