{"entities":{"Q2751353":{"pageid":2762092,"ns":120,"title":"Item:Q2751353","lastrevid":47693929,"modified":"2026-01-02T11:11:22Z","type":"item","id":"Q2751353","labels":{"en":{"language":"en","value":"Resolution theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1664641"}},"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":"Q2751353$12CA9662-0038-4DCA-A258-C6E2F55E34D6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d1eed39d9496ec81272099c7627b650b7ad8f241","datavalue":{"value":"0993.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$FF5990B7-8ED3-45E3-96BF-96FA83821302","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0cf815526c4f2604ee47e98322610a52470dc8b3","datavalue":{"value":{"entity-type":"item","numeric-id":1072370,"id":"Q1072370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751353$2D6F54E8-371C-4BC4-9771-367893198807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b043e7c633006f3fac5c3bfd0395a92f663b5539","datavalue":{"value":{"entity-type":"item","numeric-id":758210,"id":"Q758210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751353$C51DE507-377A-4F19-8F70-9C350303B01D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"370aefb578ce7bca6fa1f7031f804823865eb545","datavalue":{"value":{"time":"+2002-08-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2751353$4353D19C-8046-4EA9-A885-D1E0C1C1587B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$F5A08775-C73F-442C-A869-4308D213D429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$2FDD5E00-2E1F-4260-9265-3D267FA86557","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89663cdc2c9f64b2cd0a104bcac86329d89b9b2d","datavalue":{"value":"03-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$033AF92D-9050-48B2-8F3D-9A1EEB0D5C1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$7E1D3143-CE52-420F-9AEB-D97B385B65BF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c891f8db304be7b274633914233465b0de87601e","datavalue":{"value":"1664641","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751353$E368953B-C16A-48C4-AC0E-4A12DB43CBAB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"421a43f4b0e8832a026eaa34353c95869f115bee","datavalue":{"value":"survey","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751353$0AAEBFC3-482E-4A3F-B8D5-862C30B01AC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"384911a23d3bae024ee09485d14b557ec1109507","datavalue":{"value":"resolution-based theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751353$8870A648-2AC0-41D6-AD87-18EADDE6C412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ab12ff58d856acb9d7004adbd35a93e62a7c0a6","datavalue":{"value":"resolution refinements","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751353$A0906209-A1C5-499A-BCA5-CCFCFADC202E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"28fc44048eed4045d16edfaea8cbc72a8cf041e0","datavalue":{"value":"resolution strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751353$ADCA9F91-1922-4887-B617-05106DEF873C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3002e5aece34ca8a020af27ced77e73776ebb698","datavalue":{"value":{"entity-type":"item","numeric-id":53728,"id":"Q53728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751353$03B57D0C-1080-4666-9B39-7D62F145C9BF","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":"Q2751353$C988DC7F-0272-401B-BE26-52EE9CA51129","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2fa1fb19e89f2fa211b17c2941594b1d468ee018","datavalue":{"value":{"text":"Resolution theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2751353$5457F89E-B446-43FA-A7E6-A42FDCDB7679","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"963f9295cc122d71d9401c37e1203a0825c2765c","datavalue":{"value":"The paper gives an extensive overview on resolution-based theorem proving. It discusses various resolution refinements and resolution strategies (by introducing orderings) for improving efficiency, and for dealing with special classes of clauses. First-order resolution methods can then be derived from ground resolution and the technique of ``lifting''.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751353$B13606FC-B8FB-4CF3-BE08-E4AE73F0E1CA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2398eef9efd57113e53ce4e1c6dc78ad09f83c74","datavalue":{"value":{"entity-type":"item","numeric-id":4942004,"id":"Q4942004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef52aedf082959589a7ba4afbc7430250d073bc1","datavalue":{"value":{"amount":"+0.8227424621582031","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":"Q2751353$8D87EEB5-EC63-468B-9300-4560C5A0A16E","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":"ef52aedf082959589a7ba4afbc7430250d073bc1","datavalue":{"value":{"amount":"+0.8227424621582031","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":"Q2751353$B2174C4E-FB4E-4E46-99A5-58F006CD19B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72a42fe5b10cd7a85cb73b625a16f6530f794c72","datavalue":{"value":{"entity-type":"item","numeric-id":2385426,"id":"Q2385426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fadd5ae5c1d33ee1846eb6b957b85dcdb2d899b","datavalue":{"value":{"amount":"+0.8218916058540344","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":"Q2751353$A97BDDED-4A52-43D1-8432-D7608A41794F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"564012405708b6c6f09a5efd00b2e4ccd103b7dc","datavalue":{"value":{"entity-type":"item","numeric-id":5444704,"id":"Q5444704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e240a01b1419f9b83f4e886d7b1c437c6e0e418","datavalue":{"value":{"amount":"+0.814662754535675","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":"Q2751353$399AF6B7-CA69-4C32-97EA-BCAE8129F951","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edcd4b9a23103ae0e3a8ef4d77f50344631b00fc","datavalue":{"value":{"entity-type":"item","numeric-id":3765263,"id":"Q3765263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f04e0453c9869d5be23aa9a15b18efe3475e981","datavalue":{"value":{"amount":"+0.8138942718505859","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":"Q2751353$113E1E6A-C488-4AF5-AF3F-4666CEA0C4A6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2751353","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2751353"}}}}}