{"entities":{"Q908895":{"pageid":910743,"ns":120,"title":"Item:Q908895","lastrevid":65326167,"modified":"2026-04-12T01:49:41Z","type":"item","id":"Q908895","labels":{"en":{"language":"en","value":"What is the inverse method?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4135910"}},"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":"Q908895$CB56681D-E6E3-4A22-BC02-A4E566445616","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fb8f491916c00ccec922d0a25617259517ef606f","datavalue":{"value":{"text":"What is the inverse method?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q908895$23C1EEB5-8166-4121-A354-4966CD28A515","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"da493453821f9a01f895d21fa3298ca101466e63","datavalue":{"value":"0694.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$53E41EB8-5496-46B9-8718-CC473F67439A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7fb080bce21f335668e348a07d25402b5a075bc7","datavalue":{"value":"10.1007/BF00245018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$C301EA84-C0F6-4633-9B8D-D7822C126737","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"264349f01f15aafc786d236704010273459ca31a","datavalue":{"value":{"entity-type":"item","numeric-id":234724,"id":"Q234724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908895$A5A7CD6A-F610-498F-8A2B-AF51E53FEAA5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q908895$A7E473D2-5840-47E5-9C73-93FFCB2BE231","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q908895$B6E44C98-F0ED-4972-A20C-83393E9E7806","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bbbd7436896b97aa59cd7bfc5dab68a9a3a87645","datavalue":{"value":"The inverse method is a method of theorem proving in predicate calculus, invented by S. Maslov in 1964. It uses a special normal form of the formula, unification and search for contradiction much like the resolution method. The derivable objects, superclauses, are disjunctions of conjunctions. There are two derivation rules, A) generating tautologies from unifiable parts of the formula, and B), close to clash- resolution:  \\[  \\frac{A_ 1\\vee D_ 1,...,A_ n\\vee D_ n}{sD_ 1\\vee...\\vee sD_ n}s\\quad =\\quad MGU(A_ 1,...,A_ n).  \\]  The difference between the presented view of the inverse method and the traditional view is explained. The difference would, however, be substantial, if ordinary clause form, not the form with superclauses were used. The inverse method is also treated in a paper by \\textit{N. K. Zamov} [Ann. Pure Appl. Logic 42, No.2, 165-194 (1989; Zbl 0692.03009)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q908895$B4384181-3FB2-4A79-9C5E-B32FEE283486","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$D4FDDB4E-A6BE-4E00-A635-4F9F593F9BF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$4405D223-467B-44C0-A337-E00C1F53BCDB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4af7ef112b5827ed97af9716aa561694c68b17e4","datavalue":{"value":"4135910","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$65011034-EF34-4480-81B6-5A94BE5B7A62","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f3e52067a7ed3ce53605a49bd0992ac3d371713","datavalue":{"value":"inverse method","type":"string"},"datatype":"string"},"type":"statement","id":"Q908895$79F84CA3-7501-4E43-AF60-7242FC13C75D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aedcb3ddc6f42b926bb2fda3b0572a51da92fbd8","datavalue":{"value":"theorem proving in predicate calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q908895$BD54D807-F563-4CB1-A3D0-47C2694650C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q908895$5CA94F75-0A9E-4E25-9E81-B29D61B884E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01240d9d606bd8eb2b8fefe121fc446c8674f072","datavalue":{"value":"superclauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q908895$D757C354-9C16-4E87-886F-ED699B43A806","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":"Q908895$4F758FD5-7F27-4050-AAEC-6FA09C2E2141","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8ba4a22c8a1b8fdd670a2b8bbdfd5dfb29eb3128","datavalue":{"value":"https://doi.org/10.1007/bf00245018","type":"string"},"datatype":"url"},"type":"statement","id":"Q908895$9307EABA-9B8C-4524-8223-C4BB7ECD7D3A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5061b51521415065123e2d5507ff73a3575c7e0b","datavalue":{"value":"W2055466270","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q908895$51C83634-2E08-43BB-B6BC-28E920B960B0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"925d527eba8bd0962c24654fc0d631c574353f48","datavalue":{"value":{"entity-type":"item","numeric-id":2751355,"id":"Q2751355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2709f42f6ca7418f1d7e9b29202da67476544a0","datavalue":{"value":{"amount":"+0.803315281867981","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":"Q908895$7D77A7C9-B54E-4E77-AC9E-7039356D5ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b60987f4308e6d760c738e339de34391092a3b0d","datavalue":{"value":{"entity-type":"item","numeric-id":3586019,"id":"Q3586019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2709f42f6ca7418f1d7e9b29202da67476544a0","datavalue":{"value":{"amount":"+0.803315281867981","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":"Q908895$2A955E6E-BA5C-46FF-B782-0CB2C5FB5421","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e629d1cd6ffbd991fdd8c8388457a782a8aefe2","datavalue":{"value":{"entity-type":"item","numeric-id":2806784,"id":"Q2806784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6646285752c2de6ca77b2d80fcee23c35141859","datavalue":{"value":{"amount":"+0.7983168363571167","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":"Q908895$A8E17CCD-510E-4C45-8003-7E53EC831DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0286684136b6b9a0d522f8cd1ac32e5399b558a9","datavalue":{"value":{"entity-type":"item","numeric-id":583187,"id":"Q583187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6828d9af1b8bbb553c174216cbd1edb50b209769","datavalue":{"value":{"amount":"+0.7839853167533875","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":"Q908895$9103F2E4-22CC-4F98-A0DA-46CEE2DCBD50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20280da19a2f8ec045ce9838c8bd70d55912852f","datavalue":{"value":{"entity-type":"item","numeric-id":3749038,"id":"Q3749038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d07331e6dc4e288cc209dc65846fc3692d2566b","datavalue":{"value":{"amount":"+0.7683466672897339","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":"Q908895$862366A1-AF9A-46EF-9832-E439F6536682","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"What is the inverse method?","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/What_is_the_inverse_method%3F"}}}}}