{"entities":{"Q1115413":{"pageid":1126162,"ns":120,"title":"Item:Q1115413","lastrevid":66764163,"modified":"2026-04-12T12:41:56Z","type":"item","id":"Q1115413","labels":{"en":{"language":"en","value":"Application of the strategy of ordering disjunctives for a modification of the method of resolutions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4085613"}},"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":"Q1115413$5BEBBF7D-27EC-44CF-B91E-4D0B1A68B135","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"305e4698371036d8ce91100a69e4fac4065900ae","datavalue":{"value":{"text":"Application of the strategy of ordering disjunctives for a modification of the method of resolutions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1115413$98F368E4-C57B-484E-A8B3-364B1CAD179D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"52d3f944b1ed0a9a8228dffe0e45e6eb6a5c62e2","datavalue":{"value":"0664.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115413$61EA7030-A187-4B30-83FA-590194CE59B0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c11fd931b02150fe771f13223f6c6dd781d02623","datavalue":{"value":"10.1007/BF01097077","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115413$78B5E16C-435E-4890-82AC-8E46F351A746","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6890901344a988227b40cad8dc069885fd1556f5","datavalue":{"value":{"entity-type":"item","numeric-id":1102127,"id":"Q1102127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115413$F48D0B24-0FFF-4E9A-84E4-C7B52971B06C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"164101b92acd585ddf6ca53b10c2e6c3aab227fa","datavalue":{"value":{"entity-type":"item","numeric-id":351720,"id":"Q351720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115413$31E7BFBE-C241-4453-97BA-996F218127C5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1115413$F7C63474-28FD-4F74-B163-DB3644C8F91F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1815f3bae318ab93aca8194e72e89993ea5db34c","datavalue":{"value":"https://eudml.org/doc/68942","type":"string"},"datatype":"url"},"type":"statement","id":"Q1115413$C397C2A6-B4EE-4DF9-8A6D-19E806422EFF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ca457e826b9b375a8988945779ce1ae21b88aeab","datavalue":{"value":"A complete strategy was formulated in the author's earlier paper [Issled. Prikl. Mat. 2, 85-90 (1974; Zbl 0341.68060)] for searching for a proof in the resolution method, enabling us to establish the provability of formulas in a one-place predicate calculus, such that the ranks of terms occurring in disjunctives of the proof are not greater than 1. This strategy depends on the ordering U of literals in disjunctives, satisfying the following condition: (A) for any literals X and Y, if the literal X precedes Y in U, then for any substitution \\(\\sigma\\), the literal \\(X\\sigma\\) precedes \\(Y\\sigma\\) in U. If such an ordering U is known, then we establish the provability of formulas in the predicate calculus by the resolution method in such a way that we first eliminate those literals which do not precede the other literals in the disjunctives containing them.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115413$F9422EC8-2A6B-4355-A2CF-5F6FB06B7BF4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115413$8544BEEB-1221-4D1C-83EA-3336DF569F9F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d153f0466e789c5b4c52a35b936024623af418a6","datavalue":{"value":"4085613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115413$08D30FBE-C28D-4106-BFD1-2EEEA2763632","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c9977afeaac4d053aef4e5b5c50df2441a2faf8","datavalue":{"value":"resolution method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115413$ACE6017B-9476-4D1C-8EC1-E8A0370CBC95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8736713440bb871c6cf7547f021f327e71accd9","datavalue":{"value":"ordering disjunctives","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115413$D8A634DA-2F11-439B-975D-256A83BA3069","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"91539a3928e5d224bfabe1123ec4886f54fb2cfb","datavalue":{"value":"provability of formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115413$90246018-3798-4FD9-895D-EA671730BA32","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":"Q1115413$41AF664D-6447-4610-993F-08472FB726AF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a3439ac502b6e53cdab3f76e7360d6b532f97fc","datavalue":{"value":{"entity-type":"item","numeric-id":1115411,"id":"Q1115411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dcc9938f42c6229fbc391a1cd9eabaa1dbc0442c","datavalue":{"value":{"amount":"+0.8445279002189636","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":"Q1115413$59489ED3-0B87-49DC-8C28-4E6B18A539F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f33a29204c9778ccdae8b7aa4ac3a2ccd717dfad","datavalue":{"value":{"entity-type":"item","numeric-id":1115412,"id":"Q1115412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90d5dacbd39d33219143cc2c08f3e763c1d543e7","datavalue":{"value":{"amount":"+0.7963587045669556","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":"Q1115413$C17FF5B3-1810-42E3-A594-792BC6AB6BD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d3fc711ff705afa18a871199e5e0adb9a892360","datavalue":{"value":{"entity-type":"item","numeric-id":3553161,"id":"Q3553161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1350af3c1a0fc2f3954c0bce5ae037a23f2cd4c","datavalue":{"value":{"amount":"+0.764748752117157","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":"Q1115413$391B4924-1828-488E-ABAA-8818ECD6DC6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"054d39becb3632d24f88bb792f8989cb064dd928","datavalue":{"value":{"entity-type":"item","numeric-id":4885907,"id":"Q4885907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0a7ed15575d5f7368c2a9f87f14c7920bba1c45","datavalue":{"value":{"amount":"+0.747282862663269","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":"Q1115413$02ED4AEF-2B81-4C63-B8C7-CE6576F3500B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3002f1e123d57d656e23853b8b69ac977ab019e9","datavalue":{"value":{"amount":"+0.7419129610061646","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":"Q1115413$20AEF726-06EA-4838-B2A3-7A5AACA52FD0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Application of the strategy of ordering disjunctives for a modification of the method of resolutions","badges":[]}}}}}