{"entities":{"Q1428985":{"pageid":1439725,"ns":120,"title":"Item:Q1428985","lastrevid":48265021,"modified":"2026-01-04T04:10:15Z","type":"item","id":"Q1428985","labels":{"en":{"language":"en","value":"Reduction of Hilbert-type proof systems to the if-then-else equational logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2063137"}},"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":"Q1428985$2BF8EF73-0E17-4213-B4A6-BFA1F2C0BA31","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e48fcafdfc2037789f107d617d7dd3271e897894","datavalue":{"value":{"text":"Reduction of Hilbert-type proof systems to the if-then-else equational logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1428985$859B5BC0-F55C-4B96-9D4F-E2A345780338","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a1d31424e681461628bacd59d2a890800104b680","datavalue":{"value":"1043.03044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1428985$119111C5-74F2-4299-879F-8491664CAD88","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c05ba2a50578fe1e22312203ffa27404328b0173","datavalue":{"value":"10.1007/BF02936099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1428985$858F8E38-DC78-4DB6-8619-91DC279517EB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b1d33efb56c286c7b23fd78205e9447a8609ee9e","datavalue":{"value":{"entity-type":"item","numeric-id":389164,"id":"Q389164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$04904E6A-22B6-489C-A132-4B6778053303","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e69251ac594e715cd30473d60ecf4960f751c916","datavalue":{"value":{"entity-type":"item","numeric-id":295417,"id":"Q295417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$AC8CA2ED-2427-4D53-B3AC-56DB05DA9458","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e1cd9bf3779f6c23821bcce79ad403c8df2b71c8","datavalue":{"value":{"time":"+2004-03-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1428985$E1F208A7-665C-4510-916C-53349E303234","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8612f0dfb6937b094e08343a5bd6b3fbe2316477","datavalue":{"value":"The notion of \\(p\\)-simulation [see \\textit{S. Cook} and \\textit{R. Reckhow}, J. Symb. Log. 44, 36--50 (1979; Zbl 0408.03044)] gives a tool to measure the relative efficiency of various proof systems. In this paper the author generalizes this notion and presents a construction of the linear reduction of Hilbert-type proof systems of propositional logics to if-then-else equational logic. The construction presented is strong enough to linearly reduce first-order logic to if-then-else equational logic as well.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1428985$A7EDEED0-FC8D-4B8D-975E-BD8802E34912","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1428985$46A3AFF8-51C7-4BC7-B768-A08F897BA8A8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be83d66401e266018878222e0a9f43f7ffb84aaa","datavalue":{"value":"2063137","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1428985$3AF314FB-7184-4463-A435-250F9B0E371A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36d4535fa24c888b72134c0d168f5dd9b0551a14","datavalue":{"value":"Hilbert-type proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1428985$6FB4A3EA-E49F-4B86-A982-E46A6B75AADF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"744fd5f6b592344bd2a87ac1816bb7847861172e","datavalue":{"value":"equational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1428985$5897AE28-A71F-480D-B344-D5A9896D45D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c98af04b2bbb8e39ee65fc6cfcf4c69d0fba37f","datavalue":{"value":"relative efficiency of proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1428985$80972C18-E950-4075-978B-4165D5C03A9C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$ED932289-AE30-43A7-BCCD-3B5AFF089DF6","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":"Q1428985$C1754887-C700-4E91-BB9A-B806D7905539","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7273ec0eb958a68acc1c78fd022c2a6c6886f422","datavalue":{"value":{"entity-type":"item","numeric-id":1350509,"id":"Q1350509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$A158E3EB-4DA7-48A6-B5B8-92E840301C25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52aa539fe3a7092000ff82c5dd9bfa3ee218a8d8","datavalue":{"value":{"entity-type":"item","numeric-id":1577476,"id":"Q1577476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$0E8487CF-9A7A-4012-8485-9376E7CA55C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc37074100decec1567b589117b5998df7e079ec","datavalue":{"value":{"entity-type":"item","numeric-id":3667922,"id":"Q3667922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$7950CD82-6073-49B7-8232-67A4F0387E78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"610e52faf72b688c3bd84b1dd432e513e77092bc","datavalue":{"value":{"entity-type":"item","numeric-id":1190748,"id":"Q1190748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$3E2CF305-88B8-431F-BC62-3A2AC7546C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$67C8C094-96F1-4E97-9A70-223876DB738C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25f4a86512e0f02bf82877dbb62313fcd7fe9ed1","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$1A229ECF-77E4-427B-9DA2-BB146DB6A14F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bfde78f73cd4ff340b10ef5b040429cdc807915","datavalue":{"value":{"entity-type":"item","numeric-id":4075454,"id":"Q4075454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$4A662378-4CB0-409E-8AE3-FCED82B92701","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fe1dde5ef1db9efebbfff6a92aedf602f03722","datavalue":{"value":{"entity-type":"item","numeric-id":3801055,"id":"Q3801055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$45102AA9-6E71-4518-A1F0-C3EF1B603CF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46c3df03f1a2987977466dbdd6d02f2af5a8e45b","datavalue":{"value":{"entity-type":"item","numeric-id":4381398,"id":"Q4381398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$782CCFFD-D43E-4746-9F4E-A3625FF65412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c88ba7ec62a74a120649025590522149f9c71c7","datavalue":{"value":{"entity-type":"item","numeric-id":1263584,"id":"Q1263584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1428985$873BFFF1-96C7-41BE-B909-D4FAFDCF8757","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43db44d2a19daeb8f2c3c361338b1df38ab6c8c3","datavalue":{"value":{"entity-type":"item","numeric-id":2455258,"id":"Q2455258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"782f0aba0c2beb36f48641c45c4f8dc6a9c43870","datavalue":{"value":{"amount":"+0.7461284399032593","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":"Q1428985$4C6771E6-6E42-433C-8FDC-4E6E284BB884","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ffa2d7418e931eb671fcf01954fd4a349e35ca8","datavalue":{"value":{"entity-type":"item","numeric-id":2826389,"id":"Q2826389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ef7f4fec98ff992a88d501072359a8108e1ac7d","datavalue":{"value":{"amount":"+0.7425317764282227","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":"Q1428985$35E287E2-FA6B-4439-A21D-F0E02C1297C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bb712603a97d95c8c6f1736d1041e8ebba15328","datavalue":{"value":{"entity-type":"item","numeric-id":1709711,"id":"Q1709711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"759177e0e0c532fb9aa1ef7b86208fb8e8193791","datavalue":{"value":{"amount":"+0.7217944860458374","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":"Q1428985$210C95F9-D23E-489B-A314-EEA2DB74F594","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"940b6dcd8950abc36b845f7581e57a016e232a46","datavalue":{"value":{"entity-type":"item","numeric-id":3803081,"id":"Q3803081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53d1f182e3044dcad9c31c7c5fb40cfba979a1a8","datavalue":{"value":{"amount":"+0.7146495580673218","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":"Q1428985$3BB08EAD-DFB4-4127-A263-274057E98877","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2277ff7c41191c25c17b3cafdb32706d5effd7a","datavalue":{"value":{"entity-type":"item","numeric-id":4010371,"id":"Q4010371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7234fd653d4cc11de126a0e1a7cdfe148bdd5ce","datavalue":{"value":{"amount":"+0.7141022086143494","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":"Q1428985$1E2971BC-5845-4F6E-9D1B-72BA64B7EAD5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1428985","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1428985"}}}}}