{"entities":{"Q1102280":{"pageid":1113032,"ns":120,"title":"Item:Q1102280","lastrevid":66684015,"modified":"2026-04-12T11:55:31Z","type":"item","id":"Q1102280","labels":{"en":{"language":"en","value":"The number of proof lines and the size of proofs in first order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4049639"}},"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":"Q1102280$77394AC4-590E-41D4-983F-F8DF11213718","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5d673bb4aa39a6a476ee29690a10abad408e4592","datavalue":{"value":{"text":"The number of proof lines and the size of proofs in first order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1102280$A617202E-7276-46C4-BF27-8C74E8C8120E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"543689e4d30af94f999efeb5815294176cce1258","datavalue":{"value":"0644.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$28418509-8026-4B55-B4EF-2B3EE0BE820D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b2d720f58cf51d9eebd72320272b172f506284cf","datavalue":{"value":"10.1007/BF01625836","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$32EB34F2-6141-483F-8F6B-7A050481D1CD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4b9ae896fbf78b3fa2084fd5300754d74076f66","datavalue":{"value":{"entity-type":"item","numeric-id":226860,"id":"Q226860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$B5D6CF52-ADF6-45C7-9631-E209DF1A2F74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"318018faae3560d6874b4d183002bf8aee67c872","datavalue":{"value":{"entity-type":"item","numeric-id":185618,"id":"Q185618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$3F13DD90-9E60-4526-B450-95B7722C8005","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$B6C544B5-4D77-40AC-B408-0F50B75AEEA1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1102280$EA451CEC-F6E1-4A5A-B707-E7560D3FD3C4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"737d0d1b60cb16e2d14313a4db03adeca4194fa3","datavalue":{"value":"A presentation of the results uses the particular formulation of Gentzen's well-known calculus LK as defined in \\textit{G. Takeuti}'s book [Proof theory (1975; Zbl 0354.02027 and Zbl 0355.02023)]. The size of a formula is the number of symbols in it. The size of a sequent is the sum of the sizes of formulas in the sequent. The size of a proof is the sum of the sizes of the sequents in the proof. The number of proof lines of the proof is the number of vertices of a corresponding rooted tree. The main question: Suppose a sequent \\(\\Gamma\\to \\Delta\\) of size m has a proof with k lines in LK. How can we bound the minimal size of a proof of \\(\\Gamma\\to \\Delta\\) in LK using k and m? If the sequent has a cut-free proof with k proof lines, then the paper gives an upper bound which is exponential in \\(k+m\\). In general only a primitive recursive bound in \\(k+m\\) is obtained. It is an open problem if there is a fixed time iterated exponential bound. The results are based on a reduction to the unification problem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$F1BC4D9C-1EAB-4D92-AF2E-579D0C0F4EA7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$C69EAFEB-A702-4587-AAF9-8C7490E0F208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$7DBFB3F9-DD3F-40B4-A381-721D1B89973B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fd224a4e849a8c2574613843930c395b49e6eead","datavalue":{"value":"4049639","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$B45E65DC-414D-4A7C-BFE5-86FC3921A978","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$8CE5A11A-4DDE-4E13-BB6B-50A86D04D6E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b054bbd1ef16f604df0f61144322893e5b9a2a9","datavalue":{"value":"upper bounds","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$74798EB0-3324-4B32-8D5F-4B83813A131C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e0ba49c0d7ee5eac793288f799f692b88bfeef8","datavalue":{"value":"Gentzen's calculus LK","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$136D5BC7-5885-4412-9EB8-91624353E554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c840e95face9076a645930dd74310f89e6c27f85","datavalue":{"value":"size of a formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$885C9C29-C5A4-4E0F-98DE-8022C23CB590","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01b50f40be44e4b86b13b767c949f9ce17b262de","datavalue":{"value":"size of a sequent","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$7715BED0-70B4-437A-A71C-D669BFE2CD69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4764a921dd1df0c0cb374af2bb13751caadefae3","datavalue":{"value":"size of a proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$DB594911-B2F8-4D68-AF8B-53673912E2FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b4b012c78a8fad75d0abcaafab6bc47b356764c","datavalue":{"value":"number of proof lines","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102280$2C3B8B18-A888-490F-9A60-0ED072F67BAE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9d72387a62806063eb7029252d60fe0b49b2d0e1","datavalue":{"value":"Q106785191","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102280$216DF86A-A982-4C87-92C8-EE0075E16281","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f8ed9eb7b5676e67d936495c86d88b4db3563325","datavalue":{"value":{"entity-type":"item","numeric-id":1317985,"id":"Q1317985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$12B008B1-B1BE-4B00-AE29-F37395B99B7B","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":"Q1102280$EC39F24F-B082-4BC4-A3BD-C78BE8340EB2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$9CF2A335-22B2-4C00-80A8-5E2260475324","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6faeb4dcb0a1808d000c26dadfc2438cb19d85f2","datavalue":{"value":{"entity-type":"item","numeric-id":3697944,"id":"Q3697944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$32D1FC1C-D58D-45FD-A057-CA1B4FF5E3F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7021c91f6a866e16b579f74b23aa54446a0c8938","datavalue":{"value":{"entity-type":"item","numeric-id":1150586,"id":"Q1150586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$385278B4-1B2C-4E28-928A-158CE391D784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba07dc7b075f512a5958344bc2487ab01c3f5b2f","datavalue":{"value":{"entity-type":"item","numeric-id":3786479,"id":"Q3786479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$42223D64-EA06-4506-9103-84648603D0DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e06aeba11d82d31d0908c53f7f9cab266ef5901c","datavalue":{"value":{"entity-type":"item","numeric-id":1168322,"id":"Q1168322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$9F5B7CA8-8877-48DF-82C6-88BCD6395274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f70c7f0070211df81086d4c25b73a9ca61d45c1","datavalue":{"value":{"entity-type":"item","numeric-id":5686023,"id":"Q5686023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$A8AFF3F1-9802-4265-920A-B3901B7A6485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fad684e4a5cb9a83ecdb3a28375de2828ef826dd","datavalue":{"value":{"entity-type":"item","numeric-id":3678694,"id":"Q3678694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$CD53EBDD-861A-4A62-943E-5366263EA32D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"761227e28ec3092e559c7874757d0ce5e8b995d8","datavalue":{"value":{"entity-type":"item","numeric-id":4198749,"id":"Q4198749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$8DCA2F1E-221D-4EAD-BEFC-4464D5776182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"058eea150b9df2856b4c1fa01610e8100a8e4283","datavalue":{"value":{"entity-type":"item","numeric-id":5966925,"id":"Q5966925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$F27DBA92-89DE-4A13-9A3D-D06272479C23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa011a834041a527ecea97cb500c12560c9ab895","datavalue":{"value":{"entity-type":"item","numeric-id":3335776,"id":"Q3335776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102280$F910636B-A670-4ABF-BFFE-F43EA62C7BD0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df9fbd6ff04a5bdf43ceac6460ba7d642d0b1cc7","datavalue":{"value":{"entity-type":"item","numeric-id":1577358,"id":"Q1577358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8419f10c875dd927e04e1f1299bba47f76e59de9","datavalue":{"value":{"amount":"+0.90958524","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$213B95AE-075A-4A06-9A70-BB26B14B22B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9b8f364d0ce24d4957868e5fc73a88e93d220e4","datavalue":{"value":{"entity-type":"item","numeric-id":3408152,"id":"Q3408152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70a6d45874f211e950fd344438bb6ecdaaf6e328","datavalue":{"value":{"amount":"+0.8944964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$160E15DA-DC05-4E66-8419-58E14EC4687F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1eb2102511dec07fb34f4d057bfc8c8f969e5375","datavalue":{"value":{"entity-type":"item","numeric-id":2503319,"id":"Q2503319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70a6d45874f211e950fd344438bb6ecdaaf6e328","datavalue":{"value":{"amount":"+0.8944964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$CD162A9A-7119-426D-A6BF-5692D0611E0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14ca1d21fc3a59da75c9f80dcbe13ab73c022254","datavalue":{"value":{"entity-type":"item","numeric-id":5310637,"id":"Q5310637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b04eaded94c01737fa84b73bf70249151667895","datavalue":{"value":{"amount":"+0.8879584","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$ADC739A2-51A0-4299-9089-48B26F243494","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aad654cbc3d3fd4f21ff222ba43f6260ac0b7071","datavalue":{"value":{"entity-type":"item","numeric-id":5941199,"id":"Q5941199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8e63c0553dfda6534623132a3e5b32e9f0b76c0","datavalue":{"value":{"amount":"+0.8857181","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$0ED9DB03-DA1A-449B-B825-A07135C4D667","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f9e41458dfc0f04035f722eb020181ff48d878e","datavalue":{"value":{"entity-type":"item","numeric-id":4534366,"id":"Q4534366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc36cef6b7cfec42c901c58056467838dde1fb32","datavalue":{"value":{"amount":"+0.88308036","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$C3902500-16E3-4D30-9BDD-B12FC5EDDE6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec4b4e126c2d0ced1d7e3dcc88e4ffcc7396c754","datavalue":{"value":{"entity-type":"item","numeric-id":4244309,"id":"Q4244309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"320958ad7d4ce48d3272357a52be28a9452c214f","datavalue":{"value":{"amount":"+0.87775934","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$D210284C-DBB2-4DAD-805F-8B849A72BB92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d99375d9af310691fe93cef97a2d130b782c085","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6a425f7e7a13e4043550ffa2e8b37c427a8c5da","datavalue":{"value":{"amount":"+0.8763711","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$87B0B5BC-C5EA-46F2-8709-F7ED3A312FFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d582558383118de9d65b0211933a9afadc6cadfa","datavalue":{"value":{"entity-type":"item","numeric-id":4357064,"id":"Q4357064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"554b165d989e00977d1b782362bc75aabd8446e8","datavalue":{"value":{"amount":"+0.8759426","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$073F205F-47A5-40EB-AF6D-6F00588A9268","rank":"normal"},{"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":"052b8c314c6a1c98c65d41d912fb556a082c7872","datavalue":{"value":{"amount":"+0.8728574","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1102280$B1B297D0-9533-40BD-988F-EA881C42A1BF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The number of proof lines and the size of proofs in first order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_number_of_proof_lines_and_the_size_of_proofs_in_first_order_logic"}}}}}