{"entities":{"Q1023053":{"pageid":1024901,"ns":120,"title":"Item:Q1023053","lastrevid":66639720,"modified":"2026-04-12T11:28:45Z","type":"item","id":"Q1023053","labels":{"en":{"language":"en","value":"Describing proofs by short tautologies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5563896"}},"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":"Q1023053$37A05D9A-93A2-4A60-B6A0-273D3198BD1D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e7c979201d48bf3195b317d8d57f7cfd0c3dd7e9","datavalue":{"value":{"text":"Describing proofs by short tautologies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1023053$5DE446B2-66BA-411A-816D-4BEF1A0E4475","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0a91fb190285e8e25ee9be1893990990ec5c4770","datavalue":{"value":"1172.03027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$95B0737D-FF60-41CC-8742-4C200692F03D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac16dcce5f3df8b1bf1087e5a90fdae80fa7a2e5","datavalue":{"value":{"entity-type":"item","numeric-id":402112,"id":"Q402112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$478FA66A-F156-4D5D-B9E6-D816658CF8B3","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":"Q1023053$3C01F49A-0689-4CDE-A0C3-AE83F1C23164","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"787079cd334b8c7e529712503a5fe043609e5231","datavalue":{"value":{"time":"+2009-06-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1023053$D24C413B-E51F-4AF1-A6F3-A5A9F7B3A160","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b31cf889c3406c97ca958fef64999b451a82a18d","datavalue":{"value":"It is well-known that the size of Herbrand disjunction is super-exponential in the size of a proof (with cut or modus ponens). The author provides an elegant construction of a short propositional tautology similar to Herbrand disjunction and completely encoding a given proof. Assuming that a proved formula \\(F\\) as well as every cut formula in the proof is prenex, take all quantifier-free instances \\(F_1,\\ldots,F_k\\) of \\(F\\) in the given proof, all quantifier-free instances \\(C_1,\\ldots,C_l\\) of antecedent cut formulas and all quantifier-free instances \\(D_1,\\ldots,D_m\\) of succedent cut formulas. The implication \\((\\bigvee_{i\\leq l}C_i\\rightarrow \\&_{j\\leq m}D_j)\\rightarrow F_1\\vee\\ldots\\vee F_k\\) is proved by a quantifier-free derivation which encodes the previous derivation of \\(F\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023053$217C3C20-60B8-4A29-933A-04260DD0E7E2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$529A990B-FA63-4C9D-9716-EE51E9BBACF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$CD3BF367-5F9C-4583-BEDC-59983337A073","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$8EBA0801-FC7D-4322-901F-FFB61823F8C5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7402eafda760cf44231375460732a75e9596fc38","datavalue":{"value":"5563896","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$441DFB8C-537F-4543-AD61-F358AA289DDC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023053$90BCD670-5785-4C59-8213-305434723089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a09c1984b41935c0a923dca51c0af0797d5eb50a","datavalue":{"value":"Herbrand's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023053$4F5D1204-5ECE-4FA0-BBE4-EA0CDE0FC49F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023053$BE09E662-2CEA-4601-BEC1-5E6072F5C25A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$F8705F1A-0868-4E4E-95B0-3D4093B994CF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45702294177a39ee1ff9766c01d5d14dfb7896ef","datavalue":{"value":{"entity-type":"item","numeric-id":21425,"id":"Q21425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$9DEC769A-268C-4F12-93BE-921B0C6A5C66","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":"Q1023053$6574A48B-29B9-4D1A-AF74-B7FC8761641E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b330e5db8dd65ea25e9853adb3af30fb437ee76a","datavalue":{"value":"https://doi.org/10.1016/j.apal.2008.10.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q1023053$3507EB62-A656-4C1D-BB63-5EE498861367","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b8584f2c2c73ed22d5413d15263e47972b4d4d4d","datavalue":{"value":"W1966337849","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$7FC9AC2D-640D-4E65-8893-A015752BE21A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"93bcd041174ccd48e10bcb2ce475e4ab10d2f70d","datavalue":{"value":{"entity-type":"item","numeric-id":944367,"id":"Q944367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$E8020FE0-6C7C-4089-AEC4-55544D20E8ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fbbdce3d319868b6dc8ed64beafab590c70e044","datavalue":{"value":{"entity-type":"item","numeric-id":5756761,"id":"Q5756761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$67450668-15D4-4BDE-AC2E-68C598B163AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b559e594edc07777117cb084e905ea94187a1df3","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$59482DF2-77F2-47EF-8716-326D8831731A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0508654f8dbc2c54065d5adc87d2e81f95024db","datavalue":{"value":{"entity-type":"item","numeric-id":1302302,"id":"Q1302302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$E75B20B7-99CF-4884-83C3-4C43EDE74F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1079b6d698a143d8d07f3dc7f4c3c2ed61bd0760","datavalue":{"value":{"entity-type":"item","numeric-id":5927981,"id":"Q5927981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$8C05F5D6-7876-450C-94B8-A74AB1E0F504","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":"Q1023053$8AE4394E-356F-43B2-9868-B90DE413AC90","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":"Q1023053$9ED40F9B-6218-4A3C-9954-052079A588FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb62a53671226a3f0f80156070ba8dac68f4ebb2","datavalue":{"value":{"entity-type":"item","numeric-id":5426006,"id":"Q5426006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$BEE75B43-BA5E-4A8F-8B3A-3B749AF03A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d71305c8d9d041668e564bf7f2f69f04f88a1b7","datavalue":{"value":{"entity-type":"item","numeric-id":3822154,"id":"Q3822154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$46BF902D-87A6-4F69-A872-D733BA987C7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e499c86ee0646fff12cf3f079c9131faaea7b20","datavalue":{"value":{"entity-type":"item","numeric-id":4215637,"id":"Q4215637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$E74EB80B-F784-4347-B372-6AFBE74ACF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023053$523AB290-74D9-4436-B7B0-45A6EB1D0B4C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"be31820c3ca74594b2693dc9544f5159a7a855f1","datavalue":{"value":"10.1016/J.APAL.2008.10.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023053$F5F31DB6-FDA3-44C8-B0E2-42EFDF4CD83B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe186cac75804def3c2fa703a831734e4da013d","datavalue":{"value":{"entity-type":"item","numeric-id":5361251,"id":"Q5361251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53e031ef583d1a8b1303d611cadaa740f92decf2","datavalue":{"value":{"amount":"+0.7315506339073181","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":"Q1023053$A37A4B9E-86CD-43E2-B5FC-A7A25498C5F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc195743269015154a8c4cbccb863971b682afe5","datavalue":{"value":{"entity-type":"item","numeric-id":4525273,"id":"Q4525273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa49c7bf1644a37519ebf26c3b507f02af4be33a","datavalue":{"value":{"amount":"+0.730907142162323","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":"Q1023053$D3E914A7-8B98-4078-B3F3-F468632FADBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b221097adb8151741c109487a261e170d2831a0","datavalue":{"value":{"entity-type":"item","numeric-id":2491080,"id":"Q2491080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94fd2daddfe9793120303b6d9137b1325feb53eb","datavalue":{"value":{"amount":"+0.7307408452033997","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":"Q1023053$42FA069C-B254-4361-AB47-61E8B2388A9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78e05ea5b7d7260ca535be85672730a3681c9e77","datavalue":{"value":{"entity-type":"item","numeric-id":2871477,"id":"Q2871477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3648afcf258e45b35cb847d72a09b1a14cf5ccb3","datavalue":{"value":{"amount":"+0.7304708361625671","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":"Q1023053$FCBADFBD-35FF-4750-98A4-6851AC035ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b507a1beffa9656dad09e24d3c4a8f82157c8c22","datavalue":{"value":{"entity-type":"item","numeric-id":5277826,"id":"Q5277826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec1c1be560171a727552406af3a330ed8c07a8fd","datavalue":{"value":{"amount":"+0.7282628417015076","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":"Q1023053$7E9C7103-8E1F-4824-B8ED-F64E5BFFCF9F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Describing proofs by short tautologies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Describing_proofs_by_short_tautologies"}}}}}