{"entities":{"Q1093632":{"pageid":1104384,"ns":120,"title":"Item:Q1093632","lastrevid":66952926,"modified":"2026-04-12T13:56:59Z","type":"item","id":"Q1093632","labels":{"en":{"language":"en","value":"Gentzen systems, resolution, and literal trees"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4023273"}},"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":"Q1093632$A5AAD66B-0DBB-4F3C-9811-7A3A58BA5B31","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4cfacbbdfcb5aadac49bb1d13b6d40a8f357cac","datavalue":{"value":{"text":"Gentzen systems, resolution, and literal trees","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1093632$12C13C09-7DAD-44DF-AFEB-7F207CE9E4A1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"04870b6ee1f4e3d5f9dd99f55691e85e533d09a1","datavalue":{"value":"0629.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$911CD01C-7F75-4B74-8460-402F7786523A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d666e96ce2fa8f92917e230fc2bc29c6dfb1050f","datavalue":{"value":{"entity-type":"item","numeric-id":673969,"id":"Q673969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1093632$0A0B7A4C-4C35-4C91-9093-14725CA64D8C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1093632$79A73685-3930-4BAA-A75C-B7914DC9DFB1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-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":"Q1093632$ABFD8B4D-DBEA-45DC-B585-8A74954A7906","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"31e6a45139ea9a5a5d24c68569857308ce051e82","datavalue":{"value":"The paper deals with the length of proofs in various calculi for propositional logic, in particular Gentzen's sequential calculus and the resolution method. The method employed here uses transformations between proofs in the various systems. In particular, the author exhibits a sequential calculus \\(G_ 1\\) with cut whose proofs correspond exactly to the derivations in the resolution calculus. From the complexity results we mention that the system \\(G_ 1\\) is not a polynomially bounded proof system. Other results deal with extended resolution and cut elimination; of particular interest is that eliminating cuts never substantially shortens the proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$D2B20297-D45F-4969-8B09-EE3A8D6DDE50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$5BBF55C9-115C-41DA-A722-3964BBBBA563","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$2C57561D-26F4-4B8B-BB4B-D222802281AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$A78C4F37-71AD-4EDC-89D5-E829F9D27F19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$1F99ACB0-B172-4717-9B47-4689772F9C76","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7c01ef1d9aab1be4c89b6bf8fd798347b1ad8f5c","datavalue":{"value":"4023273","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$143BDC67-E6A5-4292-B971-ED11AE0F2854","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24d315864f474bfd80feb086355d2a2070514d5b","datavalue":{"value":"length of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$1A3787CF-AF98-4ECC-99D3-B15AE54503F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2cf2329edeae19bcb56c52fcc569545fa9b58f45","datavalue":{"value":"calculi for propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$21C742F5-EA61-4514-B7CC-5FA90B70725B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ed30a4d12ac92f07392e4a8a9da9031a959fc8a","datavalue":{"value":"Gentzen's sequential calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$6F705AFE-AD3D-4F06-93BB-D5705B30FA50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$320B78D2-1441-49C6-96D9-51B366443E25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f0c23329b48b104ed3960c66a0cad0ccbc7b7f4","datavalue":{"value":"extended resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$A055886F-7546-48BC-81BA-888E19174F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1093632$3361C97E-87D0-4433-BFF3-0C0C9D8DF0C9","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":"Q1093632$9F55499D-3229-4201-B689-B6CD6DB3E419","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e98ea8c05c86f03693e53588189fa8770498586","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1093636762","type":"string"},"datatype":"url"},"type":"statement","id":"Q1093632$0B4DAEBA-8CFA-4486-A141-5CD63AED1E1A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e95462230d4eb4c6df095427b51e3f4de2c93f88","datavalue":{"value":"W2031157676","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$9D07E4EA-E0BF-4357-A993-E1517C93BBE7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"902634995e62cc36cd14f217163ae7998553ee8e","datavalue":{"value":"10.1305/NDJFL/1093636762","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1093632$63E85107-DCAF-4ED6-B615-3305D9F7A080","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42a3728eb6d6cea535db12f53a28c7233f093a8f","datavalue":{"value":{"entity-type":"item","numeric-id":1263584,"id":"Q1263584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08ae81b56cfc4c19d15ca9e18ca22cffc086a416","datavalue":{"value":{"amount":"+0.8705636262893677","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":"Q1093632$F19BE5FC-FF49-45D8-8323-8D58F2BCF6B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d096b94fda2a0ccefd424b9e7dc5f320dbc9f1f","datavalue":{"value":{"entity-type":"item","numeric-id":1353988,"id":"Q1353988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e36c8e631117cb97ad2e75487b9a33953f65088","datavalue":{"value":{"amount":"+0.8486566543579102","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":"Q1093632$366BBBC0-1233-4E07-BC13-4ED6234F08C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4ef7516fef19e6ad66dadf2480597f1ae72fc3d","datavalue":{"value":{"entity-type":"item","numeric-id":3081620,"id":"Q3081620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5051a7e84994150b9636f6f583378ae3a439abe3","datavalue":{"value":{"amount":"+0.8162594437599182","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":"Q1093632$6E6A3116-16D5-45C9-BA08-6E1CF8AD34BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87841b06f6d81884acd1204a2d1928d4d84031b9","datavalue":{"value":{"entity-type":"item","numeric-id":2534156,"id":"Q2534156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74b1c0b3cec5c3f66e6b72de8289db017832fc27","datavalue":{"value":{"amount":"+0.8117111325263977","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":"Q1093632$4C3D7A51-F936-4B67-B25E-499C2644E397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54821d0c308119635f722a0f5763584c2b30e7a2","datavalue":{"value":{"entity-type":"item","numeric-id":3972527,"id":"Q3972527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4787a0d75a6302b7ee6ee0813f8e5a5f27f31307","datavalue":{"value":{"amount":"+0.8086435198783875","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":"Q1093632$40052CF3-43CB-4833-BABF-14D2F5047029","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Gentzen systems, resolution, and literal trees","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Gentzen_systems,_resolution,_and_literal_trees"}}}}}