{"entities":{"Q2751044":{"pageid":2761783,"ns":120,"title":"Item:Q2751044","lastrevid":83089769,"modified":"2026-05-07T05:58:01Z","type":"item","id":"Q2751044","labels":{"en":{"language":"en","value":"Using resolution for testing modal satisfiability and building models"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1664327"}},"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":"Q2751044$457349A0-4CBA-41D0-BAEA-375339B63A91","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7c65ced28170249602e3b806d9915074c1667bbf","datavalue":{"value":"0984.03012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751044$B85C4713-F3A5-4F48-95DD-A8F4D675CF77","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"531bacf41fa7f19b08f4a713dec30b9d0307505b","datavalue":{"value":{"entity-type":"item","numeric-id":924722,"id":"Q924722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751044$EFFEAE28-CC71-46F3-BCB7-4DE8937D1DC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1fdb93d7789c716ce138d996005ad957d544064c","datavalue":{"value":{"entity-type":"item","numeric-id":299184,"id":"Q299184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751044$531FC69F-E696-4BF5-8CF0-9213B7CEEA6D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fb1c6756959a58d27f6df0bc0f4a2c614f247a86","datavalue":{"value":{"time":"+2001-11-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2751044$DF15E820-6AD8-4E94-BDD7-9433C92CFE82","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751044$69E30C38-BE1B-4826-AFCE-B58165E2A46A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751044$56E9EEA4-6677-448D-8706-B5B0B638DAE0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"16c1e9824113819ef7945232f54050fb054a8dda","datavalue":{"value":"1664327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751044$FFEB3E19-4B68-4740-B565-60BF3E7C45B8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$EFE45189-7254-455C-9160-AD35E0067E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d81d6971e005b6f4d22e5d988538f584446aa6da","datavalue":{"value":"satisfiability testing","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$6FDA905D-B32E-426B-88F3-49BCAAF94656","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$6A56871B-450C-4AA9-A0C8-3D903B5A56D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6030dbc9532fffb062da8570d4db393f597136c","datavalue":{"value":"translation-based resolution decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$E1A09EDE-8901-48A8-8E2C-7CB0AC275B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"867edb5f1fbdfc859e4a81b4fd3af4f5726fbfcd","datavalue":{"value":"multi-modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$2D59B9A6-D7DF-4E2F-AEAA-901078E37463","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9467ebcb99c7fb595a3708ef85ed70d4c36a7926","datavalue":{"value":"selection refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$C44A52A2-BE32-42BA-A06D-C7E6188EE5FE","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":"Q2751044$4986ABEF-1EFA-4DA1-87E7-C6BE5DB15886","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a4069381ed12f8044177b431a84f1678393ea61c","datavalue":{"value":{"text":"Using resolution for testing modal satisfiability and building models","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2751044$1AC9F859-44B9-405C-B889-55362F114B33","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"767b2b3e97e3eddfdd6e7f2511e99f4b9d92dd88","datavalue":{"value":"In this paper a translation-based resolution decision procedure for a multi-modal logic, defined over families of relations, is presented. The relations may satisfy certain frame properties. Different from previous such resolution decision procedures which are based on ordering refinements, this procedure is based on a selection refinement. The procedure has the advantage that it can be used both as a satisfiablity checker and a model builder. It is shown that tableaux and sequent-style proof systems can be polynomially simulated with this procedure.NEWLINENEWLINEFor the entire collection see [Zbl 0963.00028].","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751044$DFB2C02C-97FD-4219-9CFF-FA0A34B32ADF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afc2c9b248b5e31c2d9c118582a2d19acded508e","datavalue":{"value":{"entity-type":"item","numeric-id":1610669,"id":"Q1610669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3630866cacd1441387748c27bbc19222abc7844f","datavalue":{"value":{"amount":"+0.9183425903320312","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":"Q2751044$410D8209-4327-4D4A-B5B6-7E290F5D47F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47b6bb9dc551ba9a220b7a51f14cd07bdd3a25b7","datavalue":{"value":{"entity-type":"item","numeric-id":3704917,"id":"Q3704917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3630866cacd1441387748c27bbc19222abc7844f","datavalue":{"value":{"amount":"+0.9183425903320312","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":"Q2751044$6059F360-F2B7-4290-810F-779C802268B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65f7b269e781d4aa3c4ace2f7c3de9f877cc3c90","datavalue":{"value":{"entity-type":"item","numeric-id":4487263,"id":"Q4487263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd132d80685a594aed33c08af99f60ff471b3899","datavalue":{"value":{"amount":"+0.8377773761749268","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":"Q2751044$C8037553-2572-4DE3-ADD6-BDE10DA7FF93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f104792b223736a01f2dede804bd80df3f430f5e","datavalue":{"value":{"entity-type":"item","numeric-id":1284704,"id":"Q1284704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd8315fa05dfbfda8965b883a0a134eb8f381d6a","datavalue":{"value":{"amount":"+0.8243927955627441","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":"Q2751044$19231BE4-6DA4-4E4B-8501-A6147458E806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"588597922c70d0be936d8a4fb9ac82086f22414e","datavalue":{"value":{"entity-type":"item","numeric-id":4215602,"id":"Q4215602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6462458b32de89d55daeb7abb8c9c4c7be5ac37d","datavalue":{"value":{"amount":"+0.8192424774169922","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":"Q2751044$AC98D269-F50A-48E7-BBED-894AC579FD2F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using resolution for testing modal satisfiability and building models (scientific article; zbMATH DE number 1664327)","badges":[]}}}}}