{"entities":{"Q2469433":{"pageid":2480176,"ns":120,"title":"Item:Q2469433","lastrevid":57953388,"modified":"2026-04-03T05:35:03Z","type":"item","id":"Q2469433","labels":{"en":{"language":"en","value":"Propositional proof systems and fast consistency provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5232593"}},"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":"Q2469433$B9464287-C550-4CBB-ABA7-EC59ABE7169E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"68efad0426290efd45da7ece9286469b5336a4b1","datavalue":{"value":{"text":"Propositional proof systems and fast consistency provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2469433$AC1C8A43-9D37-4EBD-B737-5B3E4AF63D63","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ed6dad167a844cc2f29526a7e886c1cbc96de37a","datavalue":{"value":"1133.03036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$DDDA5E2F-DB13-4541-B41D-BF0ACAABC5CA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2188a88b6674acb5d2901ff8f3d0f4e479b75adb","datavalue":{"value":{"entity-type":"item","numeric-id":385072,"id":"Q385072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2469433$CB8DD349-5A48-4A4F-91CD-23D809C58808","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":"Q2469433$87635048-6F49-496A-9D35-97CF4BB4E5CA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a2f3c5ae60289bf112f9d893165d7e88387747bb","datavalue":{"value":{"time":"+2008-02-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2469433$640A5C34-677F-4627-BFE6-CFFA41E4EA56","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7a6627ccd86c79e048474c0a37bae2d032f065d2","datavalue":{"value":"https://arxiv.org/abs/2004.05431","type":"string"},"datatype":"url"},"type":"statement","id":"Q2469433$D60753F7-F1BD-4F01-BDF9-1B8940CFB126","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ef8c6f4002ad44bb8ce1dd0ae68475f2afef066e","datavalue":{"value":"The paper studies the problem of the length of proofs of finite consistency statements in first-order theories, and its relationship to propositional proof systems and the \\(\\text{NP}= \\text{coNP}\\) problem. A \\textit{fast consistency prover} (facop) is defined to be a consistent poly-time theory \\(S\\) containing some arithmetic such that for any consistent poly-time theory \\(T\\), the finite consistency statements for \\(T\\) have poly-size proofs in \\(S\\). By a result of \\textit{J. Kraj\u00ed\u010dek} and \\textit{P. Pudl\u00e1k} [J. Symb. Log. 54, No. 3, 1063--1079 (1989; Zbl 0696.03029)], such a facop exists if and only if there exists an optimal propositional proof system. The author further defines an \\textit{unlikely fast consistency prover} (ufacop) to be a consistent poly-time theory which proves the finite consistency statements \\(\\text{Con}_T(x)\\) of any consistent poly-time theory \\(T\\) in size polynomial in \\(x^e\\), where the axioms of \\(T\\) are decidable in time \\(n^e\\). It is shown that the existence of ufacops is equivalent to the existence of polynomially bounded propositional proof systems (and thus to \\(\\text{NP}= \\text{coNP}\\), by \\textit{S. A. Cook} and \\textit{R. A. Reckhow} [J. Symb. Log. 44, 36--50 (1979; Zbl 0408.03044)]). The author also shows that facops do not exist if the requirement of poly-time axiomatization of \\(T\\) (and \\(S\\)) is loosened to an r.e.\\ axiomatization.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2469433$144EFCF7-BDDB-41BF-BE4B-9209270F330E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2469433$49D5A92E-53AA-43AA-B02D-1C89CA200208","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$F8659F08-1798-48A1-A955-B212077715C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b4346faa01bb5fb0576370374d6456afd58d5666","datavalue":{"value":"68Q15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$979B99DD-4033-4526-B3DA-DB77E1A15F14","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"da56e8affa4e7a5febd97e7769251de03b4cef56","datavalue":{"value":"5232593","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$984FB87B-2E39-465E-AE82-447A4F187D05","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cda148d30785d35d64cde50aeb6c5d308ea1c8a2","datavalue":{"value":"optimal proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2469433$455AED80-1F83-4F91-ADF5-44F535150738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"034a2fc023e0f1735905992b532bd81d1320e94c","datavalue":{"value":"fast consistency prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2469433$EF07B489-E3AD-4E8D-B73D-67516281EF92","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":"Q2469433$4680AADC-8CF5-4192-A214-44F76F0D33A2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6d3072df35de6466d23de2fd6c44f3c0bdb07a8c","datavalue":{"value":"W2079616795","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$489CEFDB-B724-4548-A585-FF634A09FA23","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"dbfeb39c90727e577faeeb8d12fb87623d1fdac4","datavalue":{"value":"Q119846391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$1F0B1A5A-A757-43C8-B993-2ACEE76CD373","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8016ba9ccd4d2e5279b5b0a66ed8b21494c0d338","datavalue":{"value":"10.1305/NDJFL/1187031410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2469433$74229E2C-F056-4941-8B50-41F20FE1DD6E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd42326bc5434e4d083891f196b822f12749204d","datavalue":{"value":{"entity-type":"item","numeric-id":3091441,"id":"Q3091441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"edf317d3f7cd742ec090f4516b341a86d8f445be","datavalue":{"value":{"amount":"+0.7689227","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":"Q2469433$9726BA85-3EE9-4B08-9CB6-ECE1EAB9C412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d99375d9af310691fe93cef97a2d130b782c085","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9bbf0093b75b6a8a921a5d26528e07780570fdcf","datavalue":{"value":{"amount":"+0.76455307","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":"Q2469433$DFBB56D8-04DF-4D35-A1F1-431C52580EBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99c725820b5baf9eaa55d91d32089e48e59d850b","datavalue":{"value":{"entity-type":"item","numeric-id":4885911,"id":"Q4885911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53a0183f1d2b755b72aa26057a799de5496bfdfb","datavalue":{"value":{"amount":"+0.7632985","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":"Q2469433$D3AF7AEA-F39F-422F-99D6-C14C72F22346","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6aed5e5a885869f720bb6f8d8ceb89e10ad9499","datavalue":{"value":{"entity-type":"item","numeric-id":490660,"id":"Q490660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bcf0add4abab54334de860d63148947303d7bba","datavalue":{"value":{"amount":"+0.7611358","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":"Q2469433$6698587E-E2DF-48F3-A430-979EF0DCADB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd2c54ea03aaecb98f0ed62596f9edeaef7122c1","datavalue":{"value":{"entity-type":"item","numeric-id":3586043,"id":"Q3586043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abc3852f719a7dd6b52b6764fbaf62592a441078","datavalue":{"value":{"amount":"+0.75501466","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":"Q2469433$2874B2F1-2230-4F31-8958-7042A289CAE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"190f2233f2d410d2533b78e254de94e81d69cf9e","datavalue":{"value":{"entity-type":"item","numeric-id":5100043,"id":"Q5100043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"496e0a606ba74c596fdd984e3226ade5980bd2c8","datavalue":{"value":{"amount":"+0.74917316","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":"Q2469433$00717311-66C3-47F9-94F2-EC0431A3379B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe7e579e35267e66e222e086eb9001c9fdf736e1","datavalue":{"value":{"entity-type":"item","numeric-id":5898825,"id":"Q5898825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dde29bfcd03f66a2744570ae2f6df18294e5000c","datavalue":{"value":{"amount":"+0.748032","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":"Q2469433$6B59A571-E8DD-407F-9A0D-3533B523988B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2e5c0c45876a2d5fc2df6dd3b363275ab3522e0","datavalue":{"value":{"entity-type":"item","numeric-id":3569061,"id":"Q3569061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6ea8844501739d9ee1095c4456dc4dc26a7191d","datavalue":{"value":{"amount":"+0.74029297","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":"Q2469433$063D90B9-B6A7-464B-9D1B-B06D3BBBF2D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"580ed2424e9846e9da8bbc3a40e4cf849a4221ab","datavalue":{"value":{"entity-type":"item","numeric-id":4399249,"id":"Q4399249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa2cb92e1dde354933821e9fd9299461633ef5cf","datavalue":{"value":{"amount":"+0.7394404","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":"Q2469433$A3E7B233-1E45-486F-94CB-B081E992EE11","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2469433","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2469433"}}}}}