{"entities":{"Q1577358":{"pageid":1588098,"ns":120,"title":"Item:Q1577358","lastrevid":70745841,"modified":"2026-04-13T16:28:25Z","type":"item","id":"Q1577358","labels":{"en":{"language":"en","value":"Quantified propositional logic and the number of lines of tree-like proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1501384"}},"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":"Q1577358$53593CEB-0603-457F-9101-D0E1010DCC0A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5c1a03e266503499a05a1a5980fdb5f3fdb2bcf1","datavalue":{"value":{"text":"Quantified propositional logic and the number of lines of tree-like proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1577358$DAC2F110-F5D3-457B-9686-AAA804DD99D4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"da0ae8bc37d06c4912527cda25b44877de5181eb","datavalue":{"value":"0956.03049","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$F1104F4D-B185-40EC-A1CD-8EE5E7E58889","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"57e320459f18833925fd0cf45698e315faedbbdb","datavalue":{"value":"10.1023/A:1005281425560","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$3CED1DD6-9C90-494A-9AD6-AA3EC2E89A3B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"db2fe20e7af1bde4dc050e6d480bb6b9ca259444","datavalue":{"value":{"entity-type":"item","numeric-id":702484,"id":"Q702484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577358$C7F70B3B-25AF-415F-9732-7C36E4799622","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":"Q1577358$1C418A1F-363F-47BF-8FB7-23BF2914A198","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5d44b740cc16a5c0503e68c41530b9daa0bc7ab3","datavalue":{"value":{"time":"+2001-03-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1577358$36AA2195-FBD5-454A-9341-240F05B64E6C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f90244d836a5dbe8efe0d408cb90d67ad91b301b","datavalue":{"value":"Rules for quantifiers over propositions are added to the sequent calculus for propositional logic. The rules are formulated in the obvious way and they are similar to the usual rules for first-order quantification. In contrast, Substitution Frege systems are formulated in the sequent calculus for propositional logic as well; however, instead of the quantifier rules they feature a rule that allows for uniform substitution of propositional parameters by arbitrary propositional formulas. The introduction of the propositional quantifiers induces an exponential speed-up of proofs of propositional tautologies (with respect to the number of lines in a proof) over Substitution Frege systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$CA705C04-2C00-41D3-BDE8-F7F777A77649","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0a71a0b701b83e2fb6a5abddcef45416fab46202","datavalue":{"value":{"entity-type":"item","numeric-id":175245,"id":"Q175245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577358$A95EB9A1-5EEE-4423-A0B2-196C9021D096","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$56BE1E2F-615B-4406-B1C4-04D1BCDC11E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$A175B9E8-4553-4682-9E45-0E34F1162101","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c215f5f5b6141976d6ea6b1dc6208d6e3c237bf5","datavalue":{"value":"1501384","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$7A0EDC71-147C-4FD7-B3D6-11513CEEA24D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5dabd1d8c89859f83c987ff426061754669b3eb","datavalue":{"value":"quantified propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$56266820-BD7B-475F-854D-B6FD376CB278","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f1c629ab5abb1420e552264a227fa1b3690a1a2","datavalue":{"value":"tree-like proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$CC4E7C08-6832-4652-9E8E-4226197D4A5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aec01526d2d3b0a65db74199fe9fb685282baf2c","datavalue":{"value":"polynomial simulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$0D10014A-A68F-4B0B-9932-C65284B41111","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7849cf4967868e1682e85fd08af647be01332b1a","datavalue":{"value":"speed-up","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$B5688951-DF18-40A3-AEBA-80D7DE8D0BA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b9797db9b693bd13124f2a785bd5b46ec916ed42","datavalue":{"value":"number of lines in proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$1033E3DB-009A-498D-9917-C0B44116EA22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$7B43DC98-0FA2-4AB6-B59D-C7C89AE9DE25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ca6f9e57d08780db4643a1c76d46cda0aca52c3","datavalue":{"value":"substitution Frege systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577358$4EDD7713-C566-4476-908B-CA63F92ACA2A","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":"Q1577358$4AADE2D8-76F9-4307-8E8B-D20E89EF9739","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"90d4e3842787b1cf04217552bca26b9dc6f44c5e","datavalue":{"value":"https://doi.org/10.1023/a:1005281425560","type":"string"},"datatype":"url"},"type":"statement","id":"Q1577358$9BF33867-7D73-44BD-8202-757FFBA655D1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a8d9a696a744e71b66c679aa6325292891bcf2bf","datavalue":{"value":"W1497902529","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577358$E7EEB03D-1190-4E37-AB7B-F20A2BD7E40F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"892e0567a9b1fa2350db876f360145d289bd76e9","datavalue":{"value":{"entity-type":"item","numeric-id":5697716,"id":"Q5697716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"328084bab30072f74b3da5fd6adcd2cc2b9db7d1","datavalue":{"value":{"amount":"+0.7867478728294373","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":"Q1577358$AB25EA67-3F51-4024-BA21-E33C4657C861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"049a1fd15aed6edff729671c3a2eaecdb8eb9453","datavalue":{"value":{"entity-type":"item","numeric-id":1386671,"id":"Q1386671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db0345c049b8d41b4de92a1240045b6d4968be22","datavalue":{"value":{"amount":"+0.7812427282333374","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":"Q1577358$A65DEB02-2E0A-4638-9E5F-B50302041299","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97040c746017999b59eca5ee9e0197e24e4c2c2","datavalue":{"value":{"entity-type":"item","numeric-id":3138022,"id":"Q3138022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f858b3c129bda8514e425c6a6aab3d9304eddf1e","datavalue":{"value":{"amount":"+0.7396422028541565","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":"Q1577358$F7FE4A60-B454-4208-BBE9-A9B774399F7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a20304930accadc7fe78aaead233fbe7aa148b06","datavalue":{"value":{"entity-type":"item","numeric-id":3829548,"id":"Q3829548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aaa8b55fe9835c69abebcd5dc074c36a5d58f9f7","datavalue":{"value":{"amount":"+0.7386994361877441","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":"Q1577358$34B7C901-E0C1-4745-BF57-C7F993864ED6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantified propositional logic and the number of lines of tree-like proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantified_propositional_logic_and_the_number_of_lines_of_tree-like_proofs"}}}}}