{"entities":{"Q2259012":{"pageid":2269755,"ns":120,"title":"Item:Q2259012","lastrevid":71698911,"modified":"2026-04-13T23:58:04Z","type":"item","id":"Q2259012","labels":{"en":{"language":"en","value":"Cut-elimination: syntax and semantics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6409345"}},"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":"Q2259012$79F64B51-A79B-43BD-A44B-D1BC21C61C51","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d376bb2664f865be25e8c7704ca6e24f28d2b999","datavalue":{"value":{"text":"Cut-elimination: syntax and semantics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2259012$0F2AD228-0312-4B0F-B67C-E814F227C1AE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1ddb7eb408a9ea0440fb352e5158b6bdfcf719f2","datavalue":{"value":"1354.03086","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2259012$F9CB9D6F-0DC3-431F-96DD-FE9AE6F19FB0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ec91c84374e1970ffeb850b5b07163b4a998968b","datavalue":{"value":{"entity-type":"item","numeric-id":167059,"id":"Q167059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$46CEDD45-3A2C-4AF4-80D1-0F1C0DE4874A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53993ae6db4350dacb1d3d4f5370b18b73e58da6","datavalue":{"value":{"entity-type":"item","numeric-id":167060,"id":"Q167060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$4E045CA4-674F-4E57-AA31-7BE32F56B1A7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$E0FBAAC5-E057-4882-A21A-ED3C37C825A1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b04cbc0bd9d6002d18ef325b8d307775df0871bf","datavalue":{"value":{"time":"+2015-02-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2259012$F11E82E6-AC7B-4681-B251-F1501B1151D2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"af017d5af7ee71e65a93e2b01c164e913c0d93ff","datavalue":{"value":"This article concerns the cut-elimination by resolution (CERES) method for first-order logic [\\textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305)]. Compared with reductive cut-elimination (e.g.\\ Gentzen-/Sch\u00fctte-/Tait-style) which can be viewed as sequences of local reductions, CERES operates globally on LK-proofs. The method first converts the ancestors of cut-formulas into an unsatisfiable formula R (the \\textit{characteristic clause set}), and then a resolution refutation of R into an LK-proof with atomic cuts.  As well as providing a concise overview of CERES, the authors extend the method to incorporate semantically-defined generalisations of the cut rule. The new rules (called \\textit{deletions}) have the form  \\[ \\frac {\\Gamma_1 , \\Delta_1 \\quad \\dotsm \\quad \\Gamma_n, \\Delta_n} {\\Gamma_1, \\dotsc , \\Gamma_n} \\]  where \\(\\bigwedge_{i} (\\bigvee \\Delta_i)\\) is unsatisfiable.  The authors prove that CERES provides a procedure for uniformly eliminating deletions. This further differentiates CERES from reductive cut-elimination: there cannot exist a uniform procedure for the latter as it would yield a decision procedure for first-order validity.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2259012$6C1321CB-DF43-48EF-A5B1-6DDDF840124B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f9e0fdcb88010dc9358438c08e50b4bf5198c600","datavalue":{"value":{"entity-type":"item","numeric-id":1987217,"id":"Q1987217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$82DFF3EE-D5FC-4EE9-8876-2B7DCB80875F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2259012$61691E85-A86A-4DD8-9DD0-A248CEFFA6D8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8417e3af8c86c2b72c1cc8b00c25182490e5bb60","datavalue":{"value":"6409345","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2259012$05FF5378-E5B4-4C18-87C0-DC0C676D71FC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2259012$A0F461FC-7ACF-46BE-AD6E-355B6F936A32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0ab950d6ca522a7baddc9b072891987f10ff98dc","datavalue":{"value":"reductive methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q2259012$2D953670-0D75-49D0-9ED8-25AE4DBF23A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b2f90f5ca0bfa8c72c47a56f0443944e3e8b9df9","datavalue":{"value":"CERES","type":"string"},"datatype":"string"},"type":"statement","id":"Q2259012$FDAA5DD0-4D9A-4C85-B053-175EADE28B5E","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":"Q2259012$721D1699-54D6-4920-AAEA-F6AB1008AC06","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eb697ffc11f30ee9dd2ce12e0655c4621202212c","datavalue":{"value":"https://doi.org/10.1007/s11225-014-9563-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q2259012$29473416-4A15-4DA0-9D97-FD3997462CC0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"43a41c634d9b34f8315fac71577c41ec0924fa7e","datavalue":{"value":"W1992495792","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2259012$29484D99-BBCC-4247-96DE-A21249CEC255","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6ca373aaf79c485001675bd936a28ef2c814c6f","datavalue":{"value":{"entity-type":"item","numeric-id":2892685,"id":"Q2892685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$2AD572F7-4D78-4DE8-AAD0-773CFBBCD37D","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":"Q2259012$557E02CE-9A74-4A84-96FA-1B3B20D0C4E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbe7ca05964d4b09b50166ae769ef7441eabaf28","datavalue":{"value":{"entity-type":"item","numeric-id":2457341,"id":"Q2457341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$7D586D2D-D0B4-4971-9CC2-74D88FC688EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18b28d320f1946e7f3fd48081f2ba560ca397acb","datavalue":{"value":{"entity-type":"item","numeric-id":609451,"id":"Q609451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$71FFBC96-CAC0-4658-B164-44E337B51147","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768d63e712fe6a569fb742c3aee2dac03be6ea11","datavalue":{"value":{"entity-type":"item","numeric-id":3140631,"id":"Q3140631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$D7C9F9A8-DFEE-420D-8C6E-25C41E71EACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0f35ae7566b8bbe9c52c7114fdab5f84a63a423","datavalue":{"value":{"entity-type":"item","numeric-id":1840143,"id":"Q1840143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$E8D2A769-0256-4CAD-998C-36813C34DB56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$977F93EF-9B0D-4F1C-B6A7-28A971B05A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b880d3c8511f1d53c27d1537b521daf74193b4","datavalue":{"value":{"entity-type":"item","numeric-id":1102280,"id":"Q1102280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$B028089E-C1DD-4A21-B56C-E27D561ABF2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8755fff25bcbf365d5dd2dfde2f78f833a2371b","datavalue":{"value":{"entity-type":"item","numeric-id":4331764,"id":"Q4331764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$3598ADFA-2555-4BF1-AB36-17D042D91A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$AEB29D59-B4EE-423B-8619-979024EE614F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be85b3951fe2b4ee7f07bf10003c515b5749abc6","datavalue":{"value":{"entity-type":"item","numeric-id":5605873,"id":"Q5605873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$7C67F533-935D-4E7C-9E88-D399CD9ED007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3652d520789475601e366029ce7b257ab62a1ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5905909,"id":"Q5905909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2259012$F63F20DA-64AF-42B0-A5C1-9EAD4480089F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5a8fca1fd151230ce972a3714afab930da5b12cb","datavalue":{"value":"10.1007/S11225-014-9563-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2259012$9037320A-2B5C-4184-A625-C7FAA5BB8B64","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abede1ff1a0be2900336d947290c1b6d50095efc","datavalue":{"value":{"entity-type":"item","numeric-id":2457341,"id":"Q2457341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"917f67f46ff9edf400c6ef0553204896378d23da","datavalue":{"value":{"amount":"+0.88593364","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":"Q2259012$63D9EA6D-B03F-411F-A12A-40FAB7BD77DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a949c1887df37020eb85436a1ec2c31019214486","datavalue":{"value":{"entity-type":"item","numeric-id":5705916,"id":"Q5705916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81ab222124262e8192b4d65f6ee16771649cad11","datavalue":{"value":{"amount":"+0.8822227","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":"Q2259012$E15F263C-B1DD-4441-997C-F4FFF6893D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e708cd7b9edd1f124afe14dce1137c8bd1b31f5d","datavalue":{"value":{"entity-type":"item","numeric-id":716500,"id":"Q716500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b75cb314866d10e8f703161b9b4f8f621db7541","datavalue":{"value":{"amount":"+0.8797784","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":"Q2259012$33E0F8C9-DF6C-4952-A608-41FDC748C407","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2402b34c779a73eb9f6c4530e64b5a77c98788a","datavalue":{"value":{"entity-type":"item","numeric-id":609451,"id":"Q609451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27a0bae9ebf69709155685ca41bf7b05d5246e32","datavalue":{"value":{"amount":"+0.8709446","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":"Q2259012$9A37B283-86CE-4057-BEED-6ABBB0701AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"987183b865f4f446f72937c8f91496cd57b6c811","datavalue":{"value":{"entity-type":"item","numeric-id":5756761,"id":"Q5756761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26588b263f6fbe39fb467578b633083a0355363c","datavalue":{"value":{"amount":"+0.861848","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":"Q2259012$53E32D59-49C6-4857-B610-3F9A9B085AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a36dab317dc6184607b28b60227d46e835ea9eef","datavalue":{"value":{"entity-type":"item","numeric-id":2987066,"id":"Q2987066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80e8637092aedc63d2c1debf09d2a1d09173ddcc","datavalue":{"value":{"amount":"+0.8490773","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":"Q2259012$74B2148F-0F3D-4BDB-987B-2CFC04C8A168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dff2234d712e9ec47640c786da6a18cb4b7bcee","datavalue":{"value":{"entity-type":"item","numeric-id":5705944,"id":"Q5705944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22bc8ca9ded5fe06f4b813b7637bef6fb8f66ee0","datavalue":{"value":{"amount":"+0.8399118","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":"Q2259012$C673F16A-4C49-4B3D-92E9-F57AA85EAABD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a747b35f96986626e096eb10bb9a93b4c83ed6da","datavalue":{"value":{"entity-type":"item","numeric-id":5747781,"id":"Q5747781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1d07acaf98017ad39504a6fc8c7b7c1af68d676","datavalue":{"value":{"amount":"+0.83770996","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":"Q2259012$DD2348C0-7203-4268-933A-9AB5B01E8208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62d255f532a843485854e35c090b2b77e23e9166","datavalue":{"value":{"entity-type":"item","numeric-id":2363201,"id":"Q2363201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2ba0880134541386febf5443c5eaed9b880baa5","datavalue":{"value":{"amount":"+0.8299282","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":"Q2259012$0DF5031A-3CA9-4F63-953B-9C9C52CB0ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2de34afdb9b082773bacb814a8bd7b9258df53ec","datavalue":{"value":{"entity-type":"item","numeric-id":5505574,"id":"Q5505574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80327088a51da7c5f64d66a6777208bd287c8c51","datavalue":{"value":{"amount":"+0.8250587","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":"Q2259012$0B42C64F-F566-436A-9FDA-9371AFCEB00E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut-elimination: syntax and semantics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut-elimination:_syntax_and_semantics"}}}}}