{"entities":{"Q757094":{"pageid":758943,"ns":120,"title":"Item:Q757094","lastrevid":64103481,"modified":"2026-04-11T17:39:59Z","type":"item","id":"Q757094","labels":{"en":{"language":"en","value":"Theorem-proving with resolution and superposition"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4193157"}},"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":"Q757094$E5A33D68-4595-480E-B4CD-F78C33088AA7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"607d32ee7259bc3f6538a5e0b80f347983ea1085","datavalue":{"value":{"text":"Theorem-proving with resolution and superposition","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q757094$7AA1F266-A590-421D-8DE6-CE4310ABEF5E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aac7c25b0ee19a475d1e901e39853f2ff5607a0a","datavalue":{"value":"0723.68094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757094$C51C473D-798E-4C6C-B811-EB4D000C537C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"080da1630ed930f4aaf979061e317f2b3c0691c1","datavalue":{"value":"10.1016/S0747-7171(08)80131-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757094$9F8473BA-C2B8-4B59-B782-C0EA2682426D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$AAC6E7D7-49EB-44F8-9517-7750F9F94DDA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-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":"Q757094$13E6707A-CF1C-4316-8C91-21BF69B17FC6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757094$29462C0D-00EE-4F49-BAF4-71AEAB072E84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757094$354DE26D-29CB-4BF0-93E5-6638CD2EC8EE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc76be6e7694991b086adde04f45d2ba16226aa6","datavalue":{"value":"4193157","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757094$250D7A03-7C94-4040-979A-BF3D5D1BBC93","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q757094$A11A9267-38E8-43AE-B462-DE145D11CD84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d86a171fa82c1ea15db4e7a7c23402cbb117f3b1","datavalue":{"value":"superposition","type":"string"},"datatype":"string"},"type":"statement","id":"Q757094$AC57AE34-0D40-4D94-92DC-3AA14E6BA29D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1016db0440ddcc41c1dbed72ae746094004f63ac","datavalue":{"value":"complete simplification ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q757094$AE064361-7AF7-489C-AA7B-349884F55521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e77e9ddc2b6b581a15d6d0b0a315349c6992385","datavalue":{"value":"refutational completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q757094$1948D736-86BB-48CC-AA59-010C661B10F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q757094$3C97970E-CAB1-43AD-8CD5-7D09AF71B917","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d5450522126073beebe5b41bdc84b794c874c239","datavalue":{"value":{"entity-type":"item","numeric-id":437030,"id":"Q437030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$04551A67-A216-4329-827E-63FCEFBAFBA8","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":"Q757094$5F1883AF-8920-45BC-86B3-EE605C8A61AF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$39E6843F-6106-425B-869E-99AB5AB31DB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"378088a63ec20245823db74d6a8845609e39ce21","datavalue":{"value":{"entity-type":"item","numeric-id":593789,"id":"Q593789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$889D95F8-43AB-4BBE-BD16-1C76BEB45330","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6d3f5f0e6d39b0610560c479018fc71a2adcd20","datavalue":{"value":{"entity-type":"item","numeric-id":1098624,"id":"Q1098624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$292077B8-E348-4E01-9746-C1C19B67011B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28f9060d78a8d509e4a96bdf7415308caae8e22","datavalue":{"value":{"entity-type":"item","numeric-id":1060857,"id":"Q1060857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$A374E5F0-4458-4BED-95DD-45ECDE21199B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"041184ced68ec1bcfc7e3558db4714d4dc908858","datavalue":{"value":{"entity-type":"item","numeric-id":4050192,"id":"Q4050192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$43E3D9ED-1C25-4EA5-BBD8-469D3338D305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7819d4cde146b169662c83aab32ea4e5414cd355","datavalue":{"value":{"entity-type":"item","numeric-id":3786024,"id":"Q3786024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$6D363244-749B-4323-BDDE-F0A4FD6A1D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bc614fe187bd0295ec729cf32cb3675e34b7b37","datavalue":{"value":{"entity-type":"item","numeric-id":4302847,"id":"Q4302847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$19824C8F-D133-4305-BD9F-0ECC1F6C489B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b95a10e194b852a6f6838734d909c8312bfc826f","datavalue":{"value":{"entity-type":"item","numeric-id":3028369,"id":"Q3028369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$1CE486DE-B345-42E7-8E88-070B808729D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7dd076536f3668f703f8f8e17b2cfee8106654e","datavalue":{"value":{"entity-type":"item","numeric-id":1154801,"id":"Q1154801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$8238703D-87A5-4914-AD0F-BDBC55C6B26E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"985955d42b923cfa0515d9e4152c08273fc9f86a","datavalue":{"value":{"entity-type":"item","numeric-id":757095,"id":"Q757095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$ADCACD36-D312-4160-9351-CAC52142C83B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$D3569BAA-B2D0-4B0C-9F71-5298B43DCD41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b81bac0c83a1bb3be4d60a72c12b74b133412b10","datavalue":{"value":{"entity-type":"item","numeric-id":3702510,"id":"Q3702510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$D3AFB0EB-CC3B-42D4-9E33-51FE97E2D137","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":"Q757094$8FCDFB8E-060B-43CF-B7FA-06BABD965C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"308b028dc2f3677f2096e97af52994a72e37140b","datavalue":{"value":{"entity-type":"item","numeric-id":1820598,"id":"Q1820598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$F106C660-7870-409B-9D5C-7C06442363E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be6703352d0742c926dd615f94402f57fc94af13","datavalue":{"value":{"entity-type":"item","numeric-id":3698310,"id":"Q3698310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$FD50BC36-FA72-4286-9D62-38EB4CC860C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5939193d2c734f0c40871d2dae732bc5d8448c2d","datavalue":{"value":{"entity-type":"item","numeric-id":3673152,"id":"Q3673152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$04B9A30C-3068-4BC2-A200-EA1CA891A2F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$27BA5317-18BB-4A70-B45B-6B1145894666","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":"Q757094$0BC6E72F-B750-4652-BB7D-35D21C513927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$31C7AD9F-A065-4009-BC7A-0732501A08BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7053c119e620b9c3b3c8c19da3a6a2d1be1e3c68","datavalue":{"value":{"entity-type":"item","numeric-id":5538934,"id":"Q5538934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757094$C44D9493-8D56-4DC4-9776-DAC2E9A30765","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72f85abec70b5900edfa6c29a25c115a35cc1d65","datavalue":{"value":{"amount":"+0.8512611389160156","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":"Q757094$719D2AB6-5954-47DD-A78D-247000ADCD53","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":"72f85abec70b5900edfa6c29a25c115a35cc1d65","datavalue":{"value":{"amount":"+0.8512611389160156","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":"Q757094$CA24B5F6-765B-448B-AA66-E621C94D59DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4b1cca5b3b4f8752faa6dd4c1672915b638687e","datavalue":{"value":{"entity-type":"item","numeric-id":1060857,"id":"Q1060857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"879d7992f299a36f2e4c417de3b540004b650d73","datavalue":{"value":{"amount":"+0.850447952747345","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":"Q757094$5D114C13-51BE-4434-84F0-23CBF261EA2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d8cdcc0bc38cde26587a3338b1faf976e3f210f","datavalue":{"value":{"entity-type":"item","numeric-id":5881276,"id":"Q5881276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7bc12c2b42dd91e8154506b40802ab4fd098008c","datavalue":{"value":{"amount":"+0.837470531463623","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":"Q757094$16B54A51-C00F-4EF5-BF81-E62D0288D7EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126f7aadcf86a4abb574c1835ceb3af729a14aa9","datavalue":{"value":{"entity-type":"item","numeric-id":4255513,"id":"Q4255513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"524839149e9a463857a7f49470dbe7a5cd64accc","datavalue":{"value":{"amount":"+0.835567831993103","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":"Q757094$19DCE890-6965-4B5F-B3B1-B29868A958EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem-proving with resolution and superposition","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem-proving_with_resolution_and_superposition"}}}}}