{"entities":{"Q757093":{"pageid":758942,"ns":120,"title":"Item:Q757093","lastrevid":64103472,"modified":"2026-04-11T17:39:59Z","type":"item","id":"Q757093","labels":{"en":{"language":"en","value":"Using forcing to prove completeness of resolution and paramodulation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4193156"}},"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":"Q757093$922850DA-A870-4EFD-A670-58FE9B66611C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b620db626b472de681e13765913e63c9da42256a","datavalue":{"value":{"text":"Using forcing to prove completeness of resolution and paramodulation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q757093$04E447FC-ED03-4664-85D0-2AC412D49629","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"57208f71b17645163f67f4ce63af2489a594b945","datavalue":{"value":"0723.68093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$E7434CEF-E623-413F-B2CA-AD20916486E7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fbff432b0e24a707eec5ebe1cb4a034a2ef582b8","datavalue":{"value":"10.1016/S0747-7171(08)80130-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$A96EA9F1-D487-4886-925F-571A98A66072","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ac8dc2320e97622b1e710be45172dc57538b09e","datavalue":{"value":{"entity-type":"item","numeric-id":757091,"id":"Q757091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$8099F399-6B4F-479B-A4E4-8A87B552C8F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"328e72d2c847d33960a5c4c90013eca0c0cd7490","datavalue":{"value":{"entity-type":"item","numeric-id":757092,"id":"Q757092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$947D447F-A141-4097-9785-693228D3E199","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":"Q757093$99630F83-FE6A-4183-83D7-0AE38723AE87","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":"Q757093$9BA45FBE-4FDA-4ECD-BB6A-7F4D12017798","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$457FB1E9-69FC-4C0B-887F-6412AA0936EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$2970C7F0-E4B3-4CB5-8765-C081B2F3AA21","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a372238f2765f5e50a19311378305df63eae7610","datavalue":{"value":"4193156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$7CCAD671-77EE-4947-AFE5-7788A7D6B3D3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q757093$3CF64A27-A11D-41EB-9A18-2977CF613719","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q757093$37BA82D8-6EE5-46FB-A54D-FBCAEF9D65C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q757093$082E32F6-5F1C-4BAE-B467-53828421307C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9f81fd79d9a404edbf19c987163b4693c5a6aa6","datavalue":{"value":"first-order logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q757093$E6A9C8B9-E49B-48C0-99C9-C75176BFBC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b23248042bd506455f51600d00d7ec5443276f9","datavalue":{"value":"forcing","type":"string"},"datatype":"string"},"type":"statement","id":"Q757093$17EC562D-542E-42F2-A193-D182F8715A15","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":"Q757093$4B6D544D-A1CC-4DDC-8939-2CD177DC9C2F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"736b836520ef40f65bed421f04004e40c029fa07","datavalue":{"value":{"entity-type":"item","numeric-id":5055708,"id":"Q5055708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$9EDAB950-E162-4677-A2F5-279707981CDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0a79c64039113aead593cb0db56a07ef93be24a","datavalue":{"value":{"entity-type":"item","numeric-id":5626648,"id":"Q5626648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$C8F45901-2DD4-4BDD-B410-DAC1745D8CDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4da258b65e2346205134973cc333997cb45b7692","datavalue":{"value":{"entity-type":"item","numeric-id":5570212,"id":"Q5570212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$DECC25B8-3871-4EB7-8EEC-2AC62976514A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4fb53dc30cdc46111c93a6e7de143f2e9b39160","datavalue":{"value":{"entity-type":"item","numeric-id":4099229,"id":"Q4099229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$B12706EB-A8E0-45ED-AF0A-4509EAEB89B5","rank":"normal"},{"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":"Q757093$A90AF759-2131-4BF5-AB5A-51CD45E7989A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a9e9cd00bd888e0c2ec3144ef21f154ae7d49a0","datavalue":{"value":{"entity-type":"item","numeric-id":5573370,"id":"Q5573370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$347A077B-C9DE-4D22-B8FB-C77C6E6EE4F7","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":"Q757093$3B202DA4-4571-43C7-957E-A07CECDB1649","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":"Q757093$70284D78-B8E4-49D6-BF9F-BDB0CDA21712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$87BCB079-203D-493F-B27A-1C42CD3D8F19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$02AAE36C-398C-4663-9896-67463E7B2CC2","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":"Q757093$2E9BC49A-24DA-44A1-9489-0152898D2C52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ba40b4a58b057e98dc8f17bce029d34aceb2bd5","datavalue":{"value":{"entity-type":"item","numeric-id":5532555,"id":"Q5532555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$841012B1-F21B-4256-8441-3F7C4FD43ECC","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":"Q757093$407C4758-2964-4BEA-84E1-6F7A0E1A106E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89220ab8d602c71315d6ba104b33f57b84a863d5","datavalue":{"value":{"entity-type":"item","numeric-id":790108,"id":"Q790108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$E835336B-D952-40E5-A79C-D8EADCF71E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd2f6870b7c939f8a2d8bc8c2761e4f62e066ec8","datavalue":{"value":{"entity-type":"item","numeric-id":3337413,"id":"Q3337413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$D40231F8-5A79-4E64-9D39-685BDAD580FE","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":"Q757093$81965055-452F-44FB-ABEC-424137357C13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"610c4ce18d93717aed8fea0917044e5effb66f85","datavalue":{"value":{"entity-type":"item","numeric-id":3962956,"id":"Q3962956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$9129CF51-BBE8-48AF-98A1-15C806F30313","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":"Q757093$B3E3B084-64E4-4ED2-9665-A9AD0DBB4A17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98782dca1b1c9d3479c56bc90f4cd51924e8bc96","datavalue":{"value":{"entity-type":"item","numeric-id":5734410,"id":"Q5734410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$EB481367-1C24-4411-8A68-82B4F1CC15F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80a3fc9b550b69a3ea2b64abeaba61a7f393a893","datavalue":{"value":{"entity-type":"item","numeric-id":5613180,"id":"Q5613180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$364DBDCA-7672-44C7-B47D-3ABBDBADBD85","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":"Q757093$13C9F7BF-721D-494E-AB72-82A13635C48A","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":"Q757093$465BEF66-2848-468A-9C16-CABAE2547662","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ebefb56013d1eec876e07a6ceb0c59107285c937","datavalue":{"value":{"entity-type":"item","numeric-id":757094,"id":"Q757094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$196F8437-F608-43C0-8F74-CE9CCF22E790","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6535d94d23ff0eec0127389bd92a68db23e45ad7","datavalue":{"value":{"entity-type":"item","numeric-id":3221027,"id":"Q3221027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$2760C8A4-8F79-48B7-A1E2-4F9BB52F6880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a00d494a72da53d5edc71ee57582c397b68b035","datavalue":{"value":{"entity-type":"item","numeric-id":3789100,"id":"Q3789100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q757093$829F0382-9D34-452E-987F-58172FA73E8C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"763ce1fcc2ff056ca97531b46f77abdfa7d32b2e","datavalue":{"value":"https://doi.org/10.1016/s0747-7171(08)80130-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q757093$F0161EB7-F9C9-4936-82A4-634E4A1FE1F9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc81011ba033a7ddbfd6a90e0cc740eb9f9c9094","datavalue":{"value":"W2072984710","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q757093$530BCF6E-18D8-4BFB-8B5B-354504BACB44","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b1f80d33d2b711c1786c52beef6916c90b47ed4","datavalue":{"value":{"entity-type":"item","numeric-id":5055708,"id":"Q5055708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"747ebc3c09d47f3082857d25c26fc586c35feebc","datavalue":{"value":{"amount":"+0.7768949270248413","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":"Q757093$463BB4DE-C527-4FA8-A9EB-F4B140E0D903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3300315caebea1d75efab67bc0a04ca3d7c7808f","datavalue":{"value":{"entity-type":"item","numeric-id":4302847,"id":"Q4302847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49c10364e942e43d37b4223bd01c855a89b4972e","datavalue":{"value":{"amount":"+0.7728871703147888","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":"Q757093$E8A57EE3-AB15-4CFD-B062-26305F9A6FC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"286564eb3bc4c320c48c2ddfca71197638c1cb5b","datavalue":{"value":{"entity-type":"item","numeric-id":914411,"id":"Q914411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69567328dd8d87ff42aef74197b3bb53526d814d","datavalue":{"value":{"amount":"+0.7656404972076416","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":"Q757093$6B7819A8-501A-47F7-845D-4B27BF67DD0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663b4e5a63cb4379d9ebb8567a8fb5f4ba79e6ca","datavalue":{"value":{"entity-type":"item","numeric-id":757094,"id":"Q757094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbce605b80091f85713d5d6525e5622f1e2a13e8","datavalue":{"value":{"amount":"+0.7612113952636719","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":"Q757093$4050ACAE-C626-4A39-AC88-C879EE79F0EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99d5cba0382620fa569315341c41ee14f432c95a","datavalue":{"value":{"entity-type":"item","numeric-id":3069725,"id":"Q3069725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bc231f446b0547ec9b74a8857f2224f25598c53","datavalue":{"value":{"amount":"+0.7530160546302795","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":"Q757093$B9B7170F-0A00-4116-859F-A010C1AC03F4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using forcing to prove completeness of resolution and paramodulation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_forcing_to_prove_completeness_of_resolution_and_paramodulation"}}}}}