{"entities":{"Q1194246":{"pageid":1204995,"ns":120,"title":"Item:Q1194246","lastrevid":66830658,"modified":"2026-04-12T13:08:47Z","type":"item","id":"Q1194246","labels":{"en":{"language":"en","value":"Complexity of resolution proofs and function introduction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 64032"}},"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":"Q1194246$6D109380-43DB-4734-94DF-4ACFED69D36B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f919e95bd4cc65edf815f2afe527193d94992231","datavalue":{"value":{"text":"Complexity of resolution proofs and function introduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1194246$27763B88-9F29-4FC4-9BCF-3BE6E367283A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5071771ec42c94cc83c8094fbc2a278862fd0817","datavalue":{"value":"0769.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$8F277BEC-8A92-435C-954C-AC4357039A2E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f14fb71d62cc5787eb452e0d071e42408e915869","datavalue":{"value":"10.1016/0168-0072(92)90042-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$EC00345E-EFEB-4013-8132-438B4CEF03AB","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":"Q1194246$EFF69552-E643-4611-832B-34FB73526E4D","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":"Q1194246$B20C77CC-AD99-4534-8ABA-37BE4DAC2BAC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$9790C1CA-8135-44A3-8178-FE25E19C6B8E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-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":"Q1194246$D42A727C-36B0-4072-A164-340DD384561C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"485d8dd328e9e26502446728c4a71299256cb253","datavalue":{"value":"The function introduction rule derives from the clause \\(C=F_ 1\\lor F_ 2\\) (with free variables \\(y_ 1,\\dots,y_ k)\\) the Skolemised form of the formula \\(C'=Q_ 1 y_ 1 Q_ 2 y_ 2\\cdots Q_ k y_ k F_ 1\\lor Q_ 1' y_ 1 Q_ 2' y_ 2\\cdots Q_ k' y_ k\\), where \\(Q_ i\\) are quantifiers, \\(\\forall'=\\exists\\), \\(\\exists'=\\forall\\). Since \\(C\\to C'\\) is valid, this rule preserves unsatisfiability. Using Statman's sequence of formulas exhibiting non-elementary speed-up over Herbrand expansions, the authors obtain non-elementary speed-up over resolution for one application of the function introduction rule.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194246$C848A747-73F6-41D9-B5F9-6789276010FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$2F0E8ABA-625E-454D-8A0B-F3BD0EC663CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$DC239393-562C-40C0-92DF-BCBB6B1D3545","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"236bf4c6f8a05fac6619e1ce9bcc8810b13a3a38","datavalue":{"value":"64032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$60363A1F-88B5-433A-BD61-5FE4B850CE22","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a56e99b2250e778fb387344e365194f9f431177","datavalue":{"value":"function introduction rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194246$96F4FC1B-FD00-4E1E-B8EF-93B41A5969F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"588fe7046e7c4fa6cfcf5f49bf7209a89dba37f4","datavalue":{"value":"unsatisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194246$1D993AD4-E28B-43FE-B50F-F97070BCAFAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3342f968c178bb5350ab7d0cd78bf9a38db0de45","datavalue":{"value":"speed-up over resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194246$FC93557B-54A8-48B5-A391-FC755155BFA0","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$9AD632AA-9D90-44EB-AD21-551B35D4917C","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":"Q1194246$20E91C77-BDDE-421C-BCF9-3E3DF6A41CAA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ed4e2b73edd0e2661ebb75822eda29ecb9eb63a","datavalue":{"value":{"entity-type":"item","numeric-id":3906484,"id":"Q3906484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$64FE1603-C6D6-428F-BF8B-59DC0DAF8596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"635a32c9b77587dd5d19b39262fc5ed839345844","datavalue":{"value":{"entity-type":"item","numeric-id":3746919,"id":"Q3746919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$17D6EDFF-4FBA-43CA-A8AD-91DF7125D2AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"100e278b9e1b9b0906d00edd93cd825724895304","datavalue":{"value":{"entity-type":"item","numeric-id":3727949,"id":"Q3727949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$5B750056-75CD-4E40-9A75-EAE44FB1FD3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cd9a63eeff6ecdf47b636cc932d1b2c195f2c43","datavalue":{"value":{"entity-type":"item","numeric-id":5393372,"id":"Q5393372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$BB42F233-1A99-4A17-AC2C-899802363689","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2c2b382c3725436e250ac6e5f951d42a292c14","datavalue":{"value":{"entity-type":"item","numeric-id":3954845,"id":"Q3954845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$49CBC6A6-DF11-48FB-88F3-4EB45E54F99C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f20e02bb907f90cb22a0a676f448fd7139f7410","datavalue":{"value":{"entity-type":"item","numeric-id":2547495,"id":"Q2547495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$2B6335E5-431D-4931-AEA2-A48F7AAFB3BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a85302529ae8048931d942accdfde415f39d0d59","datavalue":{"value":{"entity-type":"item","numeric-id":2554609,"id":"Q2554609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$9E6AD72F-FDA7-440D-BB29-4672E7F1EC23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b8154126bb7dcff376a3fb5230eefc60388d66","datavalue":{"value":{"entity-type":"item","numeric-id":5652222,"id":"Q5652222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$1651E395-9CF2-4110-BDA4-163CC328CB98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$BE3688A9-2B2D-427C-9E6D-552D68625BEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$408359BE-646C-47C4-B416-A1B5F218A46E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d63adcf83db3cf7a069d191680650dad11d4a262","datavalue":{"value":{"entity-type":"item","numeric-id":3789526,"id":"Q3789526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$59B14137-9AAF-41B8-9BBA-6940283AFA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$72B5F989-63D6-46F0-BFBB-63906ADFC0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$3F120926-1C74-4FDA-A684-8890FC907151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cceee8a5fb32e6eb7443356542ae558c36b13a21","datavalue":{"value":{"entity-type":"item","numeric-id":5672214,"id":"Q5672214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$4FE72DDD-B524-4386-BCE4-5C839B3CCF87","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":"Q1194246$404D16B3-C15C-4A93-94FD-5028DFD8E4EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1813c495b4019dbc5a0338bf865711982b775489","datavalue":{"value":{"entity-type":"item","numeric-id":4198750,"id":"Q4198750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$4016D550-4D95-4C64-90DB-DC25738C726D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194246$F17F9E25-6F3F-44CA-AD18-7820C57C63E7","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"b7fe541bcfe64c18dbeef09145542510ea100587","datavalue":{"value":"Q127087504","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194246$3BD740A5-9844-489E-9D4C-71A489AB5E68","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b543fd1a52bfcb55b3d992d351d55b7bb739b0ae","datavalue":{"value":{"entity-type":"item","numeric-id":4282603,"id":"Q4282603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"859738d3f3051a1324d98500f7df615c3dce64c5","datavalue":{"value":{"amount":"+0.7732888460159302","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":"Q1194246$161DF9C7-D09C-46D6-A4B8-6C5B17F77C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c05ff52b80d6dbfd5dc36ac59d953a7f881a330","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b55a3480867577019dd8811aed0520ca2c6c833","datavalue":{"value":{"amount":"+0.7099197506904602","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":"Q1194246$9A52F823-04FD-44CC-A80E-0BE2C4D178BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c482adf03ff0fc13be71b2497493bb138c574b48","datavalue":{"value":{"entity-type":"item","numeric-id":4863690,"id":"Q4863690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f72f75846d0e9205f2a1fc145dd1c323cc34909","datavalue":{"value":{"amount":"+0.7071025371551514","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":"Q1194246$E68737EB-13B2-4B40-BAB3-337B7848FC87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8fad119391ac0650fa8016c1ceba6481f2374b2","datavalue":{"value":{"entity-type":"item","numeric-id":3777987,"id":"Q3777987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85a6138abcd581170ba96d4fc9c4d4d47ee8286b","datavalue":{"value":{"amount":"+0.7065962553024292","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":"Q1194246$97E101C2-EF2F-4353-B6DD-C0FC0B5398F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3987f987c61a53d441911f6d6995e2961a38dc4a","datavalue":{"value":{"entity-type":"item","numeric-id":2253866,"id":"Q2253866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0d667ca5bf05a7f42d63835ed2d3513f6f74170","datavalue":{"value":{"amount":"+0.7037575244903564","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":"Q1194246$FEFA905B-C3EC-40F0-B411-FBA98945F684","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Complexity of resolution proofs and function introduction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Complexity_of_resolution_proofs_and_function_introduction"}}}}}