{"entities":{"Q758218":{"pageid":760067,"ns":120,"title":"Item:Q758218","lastrevid":64149099,"modified":"2026-04-11T17:57:58Z","type":"item","id":"Q758218","labels":{"en":{"language":"en","value":"On the relation between resolution based and completion based theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4195216"}},"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":"Q758218$9CB96761-3C41-4AEB-A007-699EF0DD6F0E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1744269284e5e33219525aaab06d94dee4d06ca6","datavalue":{"value":{"text":"On the relation between resolution based and completion based theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q758218$2E5014E7-5015-40DE-8776-091FAA647A7C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3c942241eb4af883adda08427148b94859e7cd98","datavalue":{"value":"0724.68081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q758218$766A0469-4E99-4B1A-9009-62DE69F94962","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"802f3b30d94a54066eea7b35a8924e468a90b117","datavalue":{"value":"10.1016/S0747-7171(08)80135-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q758218$2E5B59C1-E84D-426B-9FD7-2B19A81966CF","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":"Q758218$F3AD4EB0-3078-4A55-A941-6E46960F8774","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":"Q758218$629D8CC1-B0AB-45E1-A698-F80E1BDA13F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q758218$E5935693-789A-44FC-8025-903E4F01A16A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q758218$F9058B9E-816D-45F8-81EB-23303E6E78F8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"47ee1500b4f21f1402f02300546117827f0f6c02","datavalue":{"value":"4195216","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q758218$78762B18-CCAD-4AA8-AB6B-E1F98B684FA0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af346a384e72cb41119c7897ce7372c11cc304a0","datavalue":{"value":"Boolean rings","type":"string"},"datatype":"string"},"type":"statement","id":"Q758218$C50EB872-FFE3-44DC-B149-BD356D277E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dad4449a765947a06827d68bf6bae39b1f0ba439","datavalue":{"value":"Completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q758218$F60F0D06-CABF-4900-B1C6-E150D2309A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d86a171fa82c1ea15db4e7a7c23402cbb117f3b1","datavalue":{"value":"superposition","type":"string"},"datatype":"string"},"type":"statement","id":"Q758218$6D032BF1-6D64-4321-9DB0-DBB3340DFCBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q758218$CB7C5BD7-04EA-40EA-B87D-85299EB727C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6c78685aea0a7d91e6d41499c27d1163c6afe98","datavalue":{"value":"refutation","type":"string"},"datatype":"string"},"type":"statement","id":"Q758218$D5A21C62-4B72-43F8-8A98-15B5962BBFB0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dcab75d64016047a02a857c2fbf6460cf97916cc","datavalue":{"value":{"entity-type":"item","numeric-id":688550,"id":"Q688550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$71D2E10C-8DA8-47E0-8C26-99E808467BE5","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":"Q758218$98FB04EC-90AA-47CE-AFF6-5FEE8B33790A","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":"Q758218$9EA4A3AB-3CBE-4604-9948-A10EDE3783E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea7cc2d45740ab37c901dca227ad5b0f233afb31","datavalue":{"value":{"entity-type":"item","numeric-id":3783627,"id":"Q3783627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$B4718F6C-507D-4922-A33F-78BF6E7698A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7814c93fd14c472a24a528c1ff4a97ba1b2c10db","datavalue":{"value":{"entity-type":"item","numeric-id":802317,"id":"Q802317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$700088C7-64AE-4E40-9E15-AADA1D87A13B","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":"Q758218$51D59D70-B7D8-493B-8AF5-593D431CE9AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8586c92c4d90a06cb521bef03111f958a597fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":5574714,"id":"Q5574714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$C5B64FC7-8262-43AE-8E0A-34B4A3180AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3fef6212c8668fb5c77a7eff0b7cc9bade0a7e69","datavalue":{"value":{"entity-type":"item","numeric-id":3765266,"id":"Q3765266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$90EDA54E-3971-47B1-AAF7-50FB0081A1C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d91275bf9130acb7463119521f9d749a9a820d09","datavalue":{"value":{"entity-type":"item","numeric-id":5599129,"id":"Q5599129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q758218$78477BB4-1B8D-4DDA-90FD-E5DF2AD3FCAC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39835574666932a9f226413e82925155b1598e01","datavalue":{"value":{"entity-type":"item","numeric-id":3338214,"id":"Q3338214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2418262812f9c0161479c7f74b6dbb9215c5339","datavalue":{"value":{"amount":"+0.8177409172058105","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":"Q758218$60571AB3-5E2F-4A63-8107-E34FE406EFB2","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":"7c783938b396c3f24ead0883e749504138e2356a","datavalue":{"value":{"amount":"+0.8040515184402466","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":"Q758218$4E6E7527-C4A1-4486-8E37-F1E7D2BFF9C6","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":"782ba9f84a6ebf35f2a7c43f3e3018522b303d87","datavalue":{"value":{"amount":"+0.7990079522132874","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":"Q758218$13FE0151-FB74-4942-8261-84FE91B2207F","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":"221b4acd4315b35b7513530f1350915a2314d470","datavalue":{"value":{"amount":"+0.7881518602371216","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":"Q758218$9FD4E479-BCA8-4C3D-8FEE-CD30935A9790","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"319e919e54ae19af5725b0d7ca2380a762f4acbd","datavalue":{"value":{"entity-type":"item","numeric-id":1182107,"id":"Q1182107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b87366a6265d254e9ff082b02348d3d4cdad0767","datavalue":{"value":{"amount":"+0.7839477062225342","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":"Q758218$C8ECF9B6-19E5-48E6-BE4C-B7C810CC5FF7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the relation between resolution based and completion based theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_relation_between_resolution_based_and_completion_based_theorem_proving"}}}}}