{"entities":{"Q1610669":{"pageid":1621409,"ns":120,"title":"Item:Q1610669","lastrevid":72328344,"modified":"2026-04-14T04:09:49Z","type":"item","id":"Q1610669","labels":{"en":{"language":"en","value":"Using resolution for testing modal satisfiability and building models"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1784330"}},"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":"Q1610669$BDCC8D2B-A132-4017-8A3E-728522B770D1","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":"Q1610669$BF2E73FC-F85E-4611-9634-39B1C91CCEE6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4b3956afeb6a83f5ab2d343c914069eda29910b5","datavalue":{"value":"1005.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$07554DF2-5BE2-400B-B093-986F933C47A5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1e3ad6a41ec27d4726363ce12ccf252c460cf4f","datavalue":{"value":"10.1023/A:1015067300005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$A56F9E3B-B3D5-40EC-9E51-AAFCF3F48FB0","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":"Q1610669$51DE86EA-7593-45CD-B987-D6DB1AEDE785","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":"Q1610669$6C20E6DC-4B91-4C2D-A5CC-C63266C6DD7A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1610669$24A1D2E5-F33B-4923-A667-9EE9B300461F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a1bc61368984c5e3500adde65887085533364de4","datavalue":{"value":{"time":"+2002-08-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1610669$BD21D84E-C2C4-4751-BC01-DE540459A687","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f796f5f0e26819ccc450ecdb0c2d7ef6f2d57af5","datavalue":{"value":"A translation-based decision procedure for a multimodal logic is presented. Specifically, the paper deals with the logic \\(K_{(m)}(\\cap,\\cup,\\smile)\\), which can be seen as an extension of the basic tense logic \\(K_t\\) with intersection and union of relations (also converse relations are allowed, but not complementation of relations). The syntax and semantics of this logic is defined, and extensions with first-order frame properties or axiom schemas are presented. The resolution framework adopted by the authors is that of \\textit{L. Bachmair} and \\textit{H. Ganzinger} [``Resolution theorem proving'', in: A. Robinson et al. (eds.), Handbook of automated reasoning, Amsterdam: North Holland/Elsevier, 19-99 (2001; Zbl 0993.03008)]. The application of resolution is done via a structure-preserving transformation into clause form, in order to keep a link between the structure of modal formulae and their translated clause form. The procedure is based on a selection refinement of resolution, adopting a different approach to ordered refinements. It is interesting to stress that the method also finds models for satisfiable input formulae. It is shown that the proposed selection-based decision procedure can polynomially simulate a tableaux calculus in the spirit of \\textit{F. Massacci} [``Simplification: A general constraint propagation technique for propositional and modal tableaux'', Lect. Notes Comput. Sci. 1397, 217-231 (1998; Zbl 0903.03012)]. The last section of the paper describes a first implementation of the selection-based resolution calculus and some experiments and comparative results. The implementation is performed as an extension of the theorem prover SPASS [see \\textit{C. Weidenbach} et al., ``SPASS v0.77'', in: The CADE-14 ATP system competion, J. Autom. Reasoning 21, No. 1, 99-134 (1998; Zbl 0916.68141), p. 113].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$B9BC6635-9081-4257-B453-F9F6C1A420CA","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1610669$84621F87-56AC-4746-8382-153327595FDE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$F1754D54-CF8F-4DD2-ADDA-5147D42FAA7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$29A7763E-3D5C-436B-9456-132A7E78B364","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$C2A93033-47B1-49E9-8C9B-0E1F8005AD36","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8666d82a03a77c26313f5f03d19715d44f362646","datavalue":{"value":"1784330","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610669$0380BACE-EF4D-4603-B2DB-8D76B024CF73","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$AE324634-AD3A-4235-A8B5-1CD8F3911786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$314E43D4-7941-494F-8ED8-1B7765984C5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$5DF3734D-C931-4DAF-B6A5-B5B641225618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45ba0550e07e04a3326d1cb7dbe398ac3d7c209d","datavalue":{"value":"tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$4A4E43AB-882A-4A98-A19E-E8E8C4F68275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"57874edeb1a8d92efa1fa31b93fbd968ea8af7d7","datavalue":{"value":"model generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$BD1D238D-4CBF-4E84-B361-13C40E55A472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$0C78494E-E63B-43DA-AC91-4A21141E2055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7369b00dcc2de789af51f57c7628c1a00a554901","datavalue":{"value":"multimodal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610669$D492F2C5-7B65-40A3-9C96-B1B794F60A0B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1610669$EE7B8F28-38D2-4F64-BE4F-12835A63A4D6","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":"Q1610669$2683980F-B4F7-4E75-AD65-9C59328BD17D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a944ed262288b3ececf0d637ca058ee4d5348cc2","datavalue":{"value":{"entity-type":"item","numeric-id":2751044,"id":"Q2751044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61ca04a73d1666b3b26a3b2358b55ceeff4c127f","datavalue":{"value":{"amount":"+0.9295009","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$6BFB2097-E595-432C-96BE-48B48CA45AA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aac08cfbacd6c40e938799ee7ed56000ad53ddee","datavalue":{"value":{"entity-type":"item","numeric-id":4928429,"id":"Q4928429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c40b18217d56573b4143b8150de485037030d2a7","datavalue":{"value":{"amount":"+0.8414748","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$6B7C1531-6491-4900-B070-A7A0F1532661","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7e2fbe7cd692e973880ac194b6c5097e242d202","datavalue":{"value":{"entity-type":"item","numeric-id":3509041,"id":"Q3509041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8dd86fe57f7521046e14f5193cc7fb1f65c8dbf","datavalue":{"value":{"amount":"+0.8351429","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$E63E9F4A-08FC-4781-96A6-CA839F6D1EBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9705111bd1a837672e44e4d2934d8d7d550f427e","datavalue":{"value":{"entity-type":"item","numeric-id":2701984,"id":"Q2701984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05a8f39e9ce5f84cb07b8e8cb87add0c61f3d9d9","datavalue":{"value":{"amount":"+0.82605803","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$3E88EA99-557F-4F63-B655-B9F7380CF5E9","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":"4f91326eb1f152ac37e243e25e94d436dbf05dcc","datavalue":{"value":{"amount":"+0.8256362","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$D45F533C-9F46-4662-B828-E4159F064EB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d33b2b81dfd8f0ee2ff4645628b2fa7d00bf6ae","datavalue":{"value":{"entity-type":"item","numeric-id":4947999,"id":"Q4947999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb2585947cce5f96562b7b5143050ee65a552a01","datavalue":{"value":{"amount":"+0.8137654","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$704A710A-E599-4FED-AB86-9717CD9C7486","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ee590fc7e4e96baf110a09e808de8be714afffc","datavalue":{"value":{"entity-type":"item","numeric-id":1181709,"id":"Q1181709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"238279cdb9017bd4ad6a2f4208cd2fe1ed707d9e","datavalue":{"value":{"amount":"+0.8092819","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$E052CDF2-0C19-4150-A9E2-BE4F5B184D21","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":"bf21ed31c5526a0ae259e6c7bb9601c5cd10838a","datavalue":{"value":{"amount":"+0.8084497","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$F12CB4EE-4C83-4CD2-A5A3-AA290C4F24FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"020c54d6c6bb01cf77a353201542ebcfc84eabce","datavalue":{"value":{"entity-type":"item","numeric-id":5256336,"id":"Q5256336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5edffa8b294421768f1ae1c1493f126c1796d964","datavalue":{"value":{"amount":"+0.8074591","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$8ED798B9-4F11-4CEF-B354-28FC790F7BF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"faa06d6539769fd18443e292a0da1fe6a99ccabf","datavalue":{"value":{"entity-type":"item","numeric-id":1199813,"id":"Q1199813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b72935c90fc9c79cc80e2b64aad3bab89c7a5db7","datavalue":{"value":{"amount":"+0.80488986","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610669$A894B192-EF05-4649-A6F7-C34069931359","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using resolution for testing modal satisfiability and building models","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_resolution_for_testing_modal_satisfiability_and_building_models"}}}}}