{"entities":{"Q5434502":{"pageid":7464066,"ns":120,"title":"Item:Q5434502","lastrevid":96203069,"modified":"2026-06-05T10:40:12Z","type":"item","id":"Q5434502","labels":{"en":{"language":"en","value":"Cut Elimination in Deduction Modulo by Abstract Completion"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5223567"}},"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":"Q5434502$35E91AB5-0AEB-43C2-AD52-0D716373BE2B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b11ba68d8f3fa704c5279d5288ca143001f3c7e4","datavalue":{"value":{"text":"Cut Elimination in Deduction Modulo by Abstract Completion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5434502$DDC96A85-75AE-4D6B-8432-8CEE6D7FE3C9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"50de4d48744fdb4dd5f9ebb92795064998180eb3","datavalue":{"value":"1132.03315","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$E7E91880-309F-41B1-A7BE-3D2171438529","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1cc854787906375534ba416292f33bf3cc6d7e6","datavalue":{"value":"10.1007/978-3-540-72734-7_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$73F19629-A831-4AE0-BA59-832DA8FC758F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d8e409b4bd2cef152800e753211d297de864b62d","datavalue":{"value":{"entity-type":"item","numeric-id":2209543,"id":"Q2209543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5434502$3BFA5410-CD4F-411D-BADE-82344B9FBF8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"67de4dcf41337233b478a60d1d06381752453e30","datavalue":{"value":{"entity-type":"item","numeric-id":857912,"id":"Q857912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5434502$7B92186A-DD8A-41BD-BBCE-3A4D2B7D08EA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6b43984c3ba3f1d3c26edd57f10023672b3ba492","datavalue":{"value":{"entity-type":"item","numeric-id":3455829,"id":"Q3455829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5434502$AF7A2314-2108-4632-8AF9-5099765136FC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"47f5704c6280b1f69fc5c7b22503b1ed12496a29","datavalue":{"value":{"time":"+2008-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5434502$297210ED-D529-4D68-98D0-0B1C31B633AD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5206d182b3e15110a2edc23ada12f7b7fdedc1ee","datavalue":{"value":"https://hal.inria.fr/inria-00115556v3/file/bk_LFCS.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5434502$58336BC6-86F2-4A4E-9BB0-1380DD6310D9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$C9A28199-2BF9-407A-86A3-F1E87E4BCBE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$F3023859-1C97-4BD3-AEC4-9475E028C31F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"436213ea9214f271a6322dada7f43968cc4d124b","datavalue":{"value":"5223567","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$8FD716A9-2EE0-476E-A510-D40FB3E4CF59","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"019a6ed5982241abb5ad173ea9f0389406288f3d","datavalue":{"value":"Knuth-Bendix completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$8E44A576-F07C-4020-8F62-5B5EBDACCD90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9bfa05c41f922906cb60d50523c1e64007b3e451","datavalue":{"value":"automated deduction and interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$F1C11E92-B0A8-481C-B6C4-281106449720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$159DE55B-F3DD-48C2-99C9-2279F45EAD1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"908a412ea1d66c8c3e12f690543d47d72647ae57","datavalue":{"value":"deduction modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$D5F2EC4F-AFA4-46AA-96D9-433CCFB67172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"218f0a3bf939f0ae69106ffbf925f06111c908b1","datavalue":{"value":"proof ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$8DADECE5-33EF-4F60-ADB1-510FBC249BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d0ec8e051fa91da37b6f8d7eaebbda7423b83b51","datavalue":{"value":"abstract canonical system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5434502$1E18CF55-D1D2-44C7-B3AD-982F85C7FE4C","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":"Q5434502$AF97E18E-271F-4E87-A8B0-5644ECE08908","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cb708affca433e544842c3e0c7e93572e26ba78d","datavalue":{"value":"W1526059592","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5434502$9C735965-96B2-4BC6-B274-54E6CE179A2E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0eed9f01c05df0977cc4b7cb2af87ba290c6703c","datavalue":{"value":{"entity-type":"item","numeric-id":2266989,"id":"Q2266989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa0dc2aa68747738e0c4f395244b1615e0a2413d","datavalue":{"value":{"amount":"+0.910638153553009","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":"Q5434502$B2784587-7462-4272-8CB6-706E73003201","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40de74ec2fd1ab65ec01cde782008815f20c8093","datavalue":{"value":{"entity-type":"item","numeric-id":5170812,"id":"Q5170812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c0c0cca1687a7fabbdfd21afc4dca06f157ed85","datavalue":{"value":{"amount":"+0.8620774149894714","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":"Q5434502$B745159A-9E05-4DCA-B3FA-5FE1A11CC433","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7ef991317cb42ba6b39ad5bd12cbd14685f436b","datavalue":{"value":{"entity-type":"item","numeric-id":3612434,"id":"Q3612434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ee4635a978b12f63365c7592a1ad3f1e1a7e11a","datavalue":{"value":{"amount":"+0.839699387550354","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":"Q5434502$B3084E64-B63E-48FB-B0D5-DBEFB5E46000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72ce4f9299c3a2986c53414825322ca224e21b8a","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45ecee40b79a19246b0d71633d3c0ac4edf84407","datavalue":{"value":{"amount":"+0.8331552147865295","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":"Q5434502$8BF74789-474F-4363-AFBA-5631B5FC521F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b42aabe80c7ceaee77425a0f3ae595e5d1a5c589","datavalue":{"value":{"entity-type":"item","numeric-id":3007658,"id":"Q3007658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"924a9ae29779ddd4ee5ff970e09db55856711b3a","datavalue":{"value":{"amount":"+0.8075563311576843","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":"Q5434502$8A4A54A0-6D78-4EC8-BC47-6FC4721FBCD2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut Elimination in Deduction Modulo by Abstract Completion","badges":[]}}}}}