{"entities":{"Q1115411":{"pageid":1126160,"ns":120,"title":"Item:Q1115411","lastrevid":66764145,"modified":"2026-04-12T12:41:56Z","type":"item","id":"Q1115411","labels":{"en":{"language":"en","value":"One modification of the ordering strategy in the resolution method"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4085611"}},"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":"Q1115411$B6A41131-7652-442E-8DDE-B521C4B09559","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0cdfe4e7c2715e7bbe566f671e48c8650d305372","datavalue":{"value":{"text":"One modification of the ordering strategy in the resolution method","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1115411$00A93919-0DF3-4A0B-8828-955B70B68ABB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1f4a38dbed77d3a4bd005c17230327be834b4bb9","datavalue":{"value":"0664.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$D7ED9916-001A-4ABD-BA5B-77A3599079BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d51783875259f6d1ebffeb765ca3dabf903618b9","datavalue":{"value":"10.1007/BF01097068","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$40E5F86D-90E5-40F4-A5FF-D429368E798A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"aa64db955f474475117f8049f4915cbb4669c50d","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115411$5C3BA89B-00BE-434D-9D0F-2246A7E282D9","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":"Q1115411$7C03BBA1-C1DE-46D6-84FD-3202D50AC102","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":"Q1115411$20276ACD-EE2B-41A0-845C-39C0EA4B7BCC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"36bcd700b171694afa8a0382deb280235e5814be","datavalue":{"value":"One of the simplest deduction search strategies in the resolution method is the strategy with ordering developed by \\textit{I. R. Slagle} [J. Assoc. Comput. Mach. 14, 687-697 (1967; Zbl 0157.024)] and \\textit{S. Yu. Maslov} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 16, 126-136 (1969; Zbl 0206.291)]. The ordering strategy restricts the choice of the principal terms for the application of the resolution rule (the R rule). In some cases, this reduces the complexity of deductions and produces decision algorithms for some decidable classes of predicate calculus.    In this note, we consider a modification of the ordering strategy and its application to the construction of a decision algorithm for one class of formulas in the predicate calculus.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115411$92E60A49-5691-4CE7-9DB6-D565B7161F08","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$C508233E-8300-4D4B-AB47-15EA32050722","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$D27D4EF7-6E06-4691-9C31-4FA5CD0BEAFF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e1372430159ee9c719dbc632e2c39a1c34988347","datavalue":{"value":"4085611","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$924F3C5E-3E44-45AD-915E-C2AAC7F3C670","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a79ab5bb2a38a4c031d7fd98f7527bfbf0be3002","datavalue":{"value":"deduction search","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115411$AC025111-3C2F-4305-ACB2-C2E9C757B05C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c9977afeaac4d053aef4e5b5c50df2441a2faf8","datavalue":{"value":"resolution method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115411$51627839-E307-4EFA-917C-BA6214072438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"558a2efcf5839176ad06dc9f495ce6fc11963b33","datavalue":{"value":"ordering strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115411$1F160EB3-B781-47BE-9EE0-C38ACEB4BF40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3018f13ec4565557bf025633f394ef25a05fe3b","datavalue":{"value":"decision algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115411$840019CC-524C-4BE0-A81D-2704BFD3A2E8","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":"Q1115411$6FAAE9D3-BE23-4A02-B5E5-53F41F14949B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f771f551f48b2f2d21f6f2011008cb21eb26e492","datavalue":{"value":{"entity-type":"item","numeric-id":5538933,"id":"Q5538933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115411$5608197F-9F00-4BE2-842D-76BFAEE46CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e963915702637e6f873c32169203d8b91d5f54c","datavalue":{"value":{"entity-type":"item","numeric-id":1217465,"id":"Q1217465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115411$4DE84103-91F2-47F9-8D8C-4E013A7F39BF","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":"Q1115411$04A175AF-5ABC-48AF-9B78-552F9AA7E3EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9d6412374cd99d26f25760aacca4ecd0fb813a7","datavalue":{"value":{"entity-type":"item","numeric-id":5339307,"id":"Q5339307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115411$4D603F6A-9C25-4534-A6A4-D2890927992F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0da12af0be0dbfdffa85df8dadc4c22ed446116c","datavalue":{"value":"https://doi.org/10.1007/bf01097068","type":"string"},"datatype":"url"},"type":"statement","id":"Q1115411$AD0DF67E-F092-42B8-8FA8-719C6A767262","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"34d6015cbdca942824a006dc26c8844d60108512","datavalue":{"value":"W2048815285","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115411$898FE9F3-F30D-4197-8C3A-98C1017F82BF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8ff25c2485666fe6d2c7ec2fca09cf34c04e31a","datavalue":{"value":{"entity-type":"item","numeric-id":1115413,"id":"Q1115413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"177da05626e6deab2d0acd899418c452d98cf15b","datavalue":{"value":{"amount":"+0.8615485","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":"Q1115411$A6F20B2A-7D8F-40BB-B1AE-C5F54858BB52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3581988c233da652609c34a0782aa2701feb66a","datavalue":{"value":{"entity-type":"item","numeric-id":1102130,"id":"Q1102130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bdb5a9366dd9e96e17612ecd5ae3856f07562f85","datavalue":{"value":{"amount":"+0.84853077","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":"Q1115411$CAAD4A69-CC00-4A0E-A4A1-52403D1CFFB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a641e18f09f25b9a649b2d550bdb655493aace2","datavalue":{"value":{"entity-type":"item","numeric-id":1390960,"id":"Q1390960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67a9115c8cfe1b8c1dd278d23d721ce06fac5c70","datavalue":{"value":{"amount":"+0.84460676","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":"Q1115411$A5B26F9E-8AC5-4424-825F-3AE6B92EEFCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b84727d90dfa94fce135de7b0d0bdde47597ea04","datavalue":{"value":{"entity-type":"item","numeric-id":1102129,"id":"Q1102129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ce8e76d5a317d9e77c673f251b73c6dab1b7e29","datavalue":{"value":{"amount":"+0.8157846","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":"Q1115411$1EFF9A3B-D796-4587-9654-BDEB49EBD2A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a86213784558f3b7600749b0cc2577359d384e4","datavalue":{"value":{"entity-type":"item","numeric-id":4282510,"id":"Q4282510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58ab1c757c305e35296d94eae39d176c3177ba88","datavalue":{"value":{"amount":"+0.81445843","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":"Q1115411$04F64063-ED70-4654-8812-1DD7CFD69AFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef4a2946459eab0b11dd23eee4e03acd0d2c1899","datavalue":{"value":{"entity-type":"item","numeric-id":2466869,"id":"Q2466869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f35b5f6e3e22d5aa51321c2ea45af31620fec80a","datavalue":{"value":{"amount":"+0.8062176","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":"Q1115411$70BD7A7B-5FED-446D-A296-A03EDDC607B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01321cacabb482e6d7f93444b91f7c8a9b896eb0","datavalue":{"value":{"entity-type":"item","numeric-id":4736520,"id":"Q4736520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"848e83817eb0ded30ee6fe00d8700dc75df36a0b","datavalue":{"value":{"amount":"+0.80093515","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":"Q1115411$06B5CE90-8945-4888-92F3-E3C303AD3723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d79de6f61a0c252c45ba92a4c364ec190f4bfd6","datavalue":{"value":{"entity-type":"item","numeric-id":1301573,"id":"Q1301573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75ab573efd6e48df4ee6aefbd0b46e6366cf19a8","datavalue":{"value":{"amount":"+0.800267","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":"Q1115411$36057C45-3E8E-4F4F-96B0-ABB37EC98AD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bec025091398a1bece0ea3c04a8b6f646ef7a31b","datavalue":{"value":{"entity-type":"item","numeric-id":4729409,"id":"Q4729409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7149a5f2779c59dff9e6aff00a589cb0a55139ad","datavalue":{"value":{"amount":"+0.7990813","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":"Q1115411$4257A66D-0543-4A2D-8EB6-85D826931375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6acacedaa7923a1afadb7acccc332f1221229d90","datavalue":{"value":{"entity-type":"item","numeric-id":3441199,"id":"Q3441199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cdb1fe924a5610d6ce0650ad371097ae9c74e5f","datavalue":{"value":{"amount":"+0.79381394","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":"Q1115411$FC53C5C9-AC96-4A6C-92FA-AE2777D60242","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"One modification of the ordering strategy in the resolution method","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/One_modification_of_the_ordering_strategy_in_the_resolution_method"}}}}}