{"entities":{"Q920970":{"pageid":922818,"ns":120,"title":"Item:Q920970","lastrevid":65361252,"modified":"2026-04-12T02:03:53Z","type":"item","id":"Q920970","labels":{"en":{"language":"en","value":"Strategies for modal resolution: Results and problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4164799"}},"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":"Q920970$8D7E8C60-46D3-46B8-9FD0-26BCF06EE086","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ab30b70fa66e5ef23386e57c30110ecc1214da4e","datavalue":{"value":{"text":"Strategies for modal resolution: Results and problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q920970$08AED93F-2C3C-418F-B209-0C6B615497E0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"54cb42dcb2b606507b2633f52440d9155ba5d94e","datavalue":{"value":"0709.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$ADC6E4C7-648F-48B5-9E26-47C1624A4D8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2343dd0de5c268ec6a49fa4ad6faadebb07e35cc","datavalue":{"value":"10.1007/BF00302639","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$25EFFA59-A0D1-45B8-A538-E509835C53B8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"513a43e5300bed081f7fd98480be32f3af92753d","datavalue":{"value":{"entity-type":"item","numeric-id":693294,"id":"Q693294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$116D2FA9-4AA5-489D-B269-BCFB6276048D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"646719c8036b1307f835e0bf21b70451a2cfe024","datavalue":{"value":{"entity-type":"item","numeric-id":920969,"id":"Q920969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$DC4E7951-0E54-4BF5-B3F9-6AD9ECFDB883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4081c4099f10e356714bb1c9f339658626e1bdda","datavalue":{"value":{"entity-type":"item","numeric-id":673673,"id":"Q673673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$7C73706D-ABBC-4322-BC36-1921441AC492","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":"Q920970$78A711C7-217B-4302-A730-7F9B4E42CAFF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-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":"Q920970$3F9F50E9-4815-4F8A-8F10-27933C402C74","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"42fedc07067ab1e45f395180dd4e41b6808d87e8","datavalue":{"value":"Automated theorem proving in modal logics, based on resolution, is a challenging problem and has caused some previous erroneous results. The authors suggest the following strategies for propositional modal logic (in fact for the S4 Kripke system): deletion of subsumed clauses, extensions of classical strategies based on a static constraint, negative resolution. A notion of a Horn clause for modal logics is introduced. An implementation of the linear strategy has already been realized. As previous related works we mention that of L. Fari\u00f1as and M. Cialdea.","type":"string"},"datatype":"string"},"type":"statement","id":"Q920970$A0B42E86-7ECC-46F4-A409-9C8A4A503660","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$98899212-8F5B-460A-9695-6E709DBF970A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$5B91F077-5B4B-4B4A-9F1A-2137B38DE1B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$D9830B3A-EBCB-45E7-8029-3A6C1F128DC5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bcf9d298c7f4b4cce6bf9c0b0b406e2cfe2bbf1f","datavalue":{"value":"4164799","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$A30C8D9B-DCFC-41CD-AAE0-59EDBAE4F929","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q920970$CC54EC8B-6BDB-413B-AC8B-4DEDF1126A16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c2ac2883b93bc6d38f9b54353e42de243081356","datavalue":{"value":"propositional modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q920970$3AED831F-14AC-4D95-A5CC-47ACA0307015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbbcce5d958a0130862ba486d8886f3214101b0c","datavalue":{"value":"S4","type":"string"},"datatype":"string"},"type":"statement","id":"Q920970$80BA9FFE-9390-4E30-B8D2-34CC6038F16D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b6c357bd39ddc429f2f5d3a98b99496258cebeb7","datavalue":{"value":"Horn clause for modal logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q920970$2447673B-073B-49B6-BBD0-DB3AF672B02F","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6536f759dee9ce142c834adc5cc137400d919eb8","datavalue":{"value":{"entity-type":"item","numeric-id":1037240,"id":"Q1037240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$0888826F-4565-478D-9F21-31AD630B56A0","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":"Q920970$A3C1C4D2-D672-4A15-9E60-0928B6E84B10","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":"Q920970$1F0CD4C8-C3FF-4BD9-9745-5B9B7ED430A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b38e00f9ec1f1ad95bd5a593d1dbecc11889a11","datavalue":{"value":{"entity-type":"item","numeric-id":1079962,"id":"Q1079962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$FA776107-859E-4373-BC69-BBCF1443EBC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e17da60b7f6b4e22bbe7045d12697c8bb0702b06","datavalue":{"value":{"entity-type":"item","numeric-id":5604443,"id":"Q5604443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920970$C9A1F064-D7BC-4485-A96C-12732D4427AE","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":"Q920970$C3126E3B-1C96-4D78-B5DD-B4D81E3CC384","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"273910ae0952b1ed72287e03f4a93e620160c8d9","datavalue":{"value":"https://doi.org/10.1007/bf00302639","type":"string"},"datatype":"url"},"type":"statement","id":"Q920970$14D29BF4-76BF-4007-AB18-E6EE574E0AAA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"524163108f93b2e4ee329418b78022af7fa0baf8","datavalue":{"value":"W2079384024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920970$719AD8B0-37D4-45AD-A296-7A90673A7C20","rank":"normal"}],"P1643":[{"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":"97c6fbdb3a6b7c566fa7d5f201a9fd3198777ac1","datavalue":{"value":{"amount":"+0.8287782073020935","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":"Q920970$EF93AFFC-7FDF-4171-ADBE-F8C908B78EE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"878c40185ef8793f4b2c6b23e206ffdc354f49d1","datavalue":{"value":{"entity-type":"item","numeric-id":3030268,"id":"Q3030268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b7ceadda84b1f59d524c9346ca71ef0edb3d688","datavalue":{"value":{"amount":"+0.8275841474533081","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":"Q920970$4C60E1C2-A5B3-41EC-9C0F-94317B1E182E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d1d80adb4ab2194e4452b04d533da571ab5ea96","datavalue":{"value":{"entity-type":"item","numeric-id":4539149,"id":"Q4539149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee0966c06e1a19bf0afa9286babe903f0c54f333","datavalue":{"value":{"amount":"+0.8178799152374268","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":"Q920970$8555C0F3-E314-44C1-B903-EC70349DA22D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92939b86137af1b0455e2845a510c8f884a99fbc","datavalue":{"value":{"entity-type":"item","numeric-id":1178699,"id":"Q1178699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c8a508e9c205e2ef38477320f32e24bac4d3ddf","datavalue":{"value":{"amount":"+0.8170580863952637","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":"Q920970$22C4EBDB-00FF-47EE-AE78-A7355FB9047C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e550364eced27e5c679bf63a38fa3b5f2670256f","datavalue":{"value":{"entity-type":"item","numeric-id":1113888,"id":"Q1113888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2934a5ab4a02daa72b0c7124b4885a0d0b7500b","datavalue":{"value":{"amount":"+0.8158377408981323","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":"Q920970$EDF3830C-B5C4-41C0-BF48-A3F2EAFAC0E0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Strategies for modal resolution: Results and problems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Strategies_for_modal_resolution:_Results_and_problems"}}}}}