{"entities":{"Q1332644":{"pageid":1343389,"ns":120,"title":"Item:Q1332644","lastrevid":70734456,"modified":"2026-04-13T16:24:17Z","type":"item","id":"Q1332644","labels":{"en":{"language":"en","value":"Resolution theorem proving in reified modal logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 627564"}},"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":"Q1332644$CE3F589C-6127-4BE0-B4B3-E6582A046C57","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a2f6da3df5bff75e50b7b3cb63e7539e6a0aadf5","datavalue":{"value":{"text":"Resolution theorem proving in reified modal logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1332644$E7C0256F-5102-47CE-8D04-6AF92762E236","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c482c93003397d419ca168a5a6452ce7349c9fce","datavalue":{"value":"0810.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$E9E1D26B-50D4-4A7D-AE30-86184B817190","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"07215a9e13a770b5061fe68d68576ede83cedc26","datavalue":{"value":"10.1007/BF00881845","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$DA725C32-FF69-48E5-89FE-77A8E1B2BB1B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"adacccd9071bbb033cf4f9ca8e9ff1475739df8b","datavalue":{"value":{"entity-type":"item","numeric-id":1332642,"id":"Q1332642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$914B0480-AA09-434A-9E3E-FE190D534525","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5fb5441c05ced2cd0f7fdf069e711f267531355b","datavalue":{"value":{"entity-type":"item","numeric-id":1332643,"id":"Q1332643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$F9C27E0E-7312-4E7D-BB94-30A428E374C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"67b2434c1778451dff4c07146a488c77497ce1ab","datavalue":{"value":{"entity-type":"item","numeric-id":814481,"id":"Q814481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$EB6A96F1-622A-46C0-8E77-5DD3A06D03CF","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":"Q1332644$6EFAB1C3-B43E-488F-AA23-B817972ED2DA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"13b74804618c57ee35b990cf82f55e89bccfb918","datavalue":{"value":{"time":"+1995-04-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":"Q1332644$2CF85E59-6FC0-4616-A61A-C2FBC5D3C031","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"94f2f75a1a90c1a2e4348ed148999e873e7cb53f","datavalue":{"value":"Non-classical logical systems are usually defined axiomatically. Set of axioms together with inference rules and rules of necessitation define a particular logic. An alternative approach is to define the semantics of the modal or temporal logic in first-order logic. This is known as the reified approach. In the reified approach to defining logical systems the semantics of the reified logics are defined by axioms in first-order logics.   The present paper presents new empirical and theoretical work on theorem proving in reified logics. The rewriting methods and world-path methods used are not new but have been used in a novel application. The advantage of the approach is that the reified logics are represented in a logical system whose semantics and proof methods are well understood. First-order logic provides a sound framework for proving theorems of a reified logic. One consequence of adopting the reified approach is that if we wish to automate proofs for modal systems, then any of the standard theorem- proving methods for first-order logic can be used to implement a theorem prover for a reified modal logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1332644$C4E4AD80-C124-48C3-A5D4-8B6456CD268F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$8CAF8C24-CE99-46F2-8627-7D1ED4437C2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$6CEE303D-32C9-4131-823F-F2E1DB781CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$A0660EAA-B066-4AEA-9F90-BDD46EAE49F0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"17c60e44e5fa29ed8d56829e9105fe4834073d4f","datavalue":{"value":"627564","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1332644$46D37A70-A4FA-46B2-8D48-1DBC56C6CD68","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b150b212b08891215d1fcd56144fe0d6275aa9e0","datavalue":{"value":"reified logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1332644$564B0674-7C20-426E-AB6C-3544A9751F75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1332644$0B0F727B-5701-4493-BEB0-29F5C43F9933","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$2D37BAD6-1269-40FD-9C6F-80835CA1A08B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4fcbbc12ff0cc07e406341b97e062f2fb672fc0","datavalue":{"value":{"entity-type":"item","numeric-id":23614,"id":"Q23614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$50BD9E35-B893-43BB-8661-729D8C9DD25A","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":"Q1332644$7803CCD3-45ED-40FA-8974-D86B76875CC6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6c4afd063e45d6804d2e85b15032fb9f38c7458","datavalue":{"value":{"entity-type":"item","numeric-id":3490986,"id":"Q3490986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$EFC6AAFA-2C43-433A-959D-004956B61B88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d4bd75352dca632f26b876b87c98f2ab5b926a7","datavalue":{"value":{"entity-type":"item","numeric-id":920970,"id":"Q920970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$AD7B4C9A-013A-4402-8718-50B88D6C91FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf4bd6f65936497199af77b410cbe7fc34d2615","datavalue":{"value":{"entity-type":"item","numeric-id":5663380,"id":"Q5663380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$F43F69D1-D6A3-406E-AD4D-4DEB1D04EC76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"925f5ecfa5a7f28801d04e2a0a5dc023244c9dab","datavalue":{"value":{"entity-type":"item","numeric-id":1181709,"id":"Q1181709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$352EA8AA-1F57-4026-8A32-326331301920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac20cbb1725a9c6c007b564f2766e3152ceda1ed","datavalue":{"value":{"entity-type":"item","numeric-id":1187214,"id":"Q1187214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$E998F202-37AB-4168-8CA9-F26A446B9124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5988b361ca37ecfb14673b33ef0fc3f5aaff39c","datavalue":{"value":{"entity-type":"item","numeric-id":3767322,"id":"Q3767322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$F59E6A4F-3970-47E1-A6BD-B8B046F839D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84e5b36bc29ceed97d7f7df9301741351cda0737","datavalue":{"value":{"entity-type":"item","numeric-id":1104913,"id":"Q1104913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$770B6138-FC81-45CF-A4AA-9CCA97B7A072","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":"Q1332644$CB066C56-2EE6-40DB-B17F-F1AD6FCAB641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5490edff7e86b453cd1c3cbf6a6a3668c1ee3881","datavalue":{"value":{"entity-type":"item","numeric-id":3992823,"id":"Q3992823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$54C21C9A-7BB4-454D-84D8-4E79A7E6C6C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23b008c640b2d8061e30defcaaf98e0ace1773df","datavalue":{"value":{"entity-type":"item","numeric-id":5339289,"id":"Q5339289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$1CDC3E7B-76F0-423F-8629-52E67E7B5C0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bade6a36335738f89d892b702a4106b53a340bf1","datavalue":{"value":{"entity-type":"item","numeric-id":3791114,"id":"Q3791114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$473BC44A-995D-4CD6-B4F4-38293EF26AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a4e10b4f29a81fca6ef84c43e9249a3d4fba6ae","datavalue":{"value":{"entity-type":"item","numeric-id":5636857,"id":"Q5636857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$E219401F-B402-4374-A317-08E3262B1D80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd7f4ac2c4d2314fae83403dbcb7eab5f78434cd","datavalue":{"value":{"entity-type":"item","numeric-id":3864488,"id":"Q3864488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$F943A99F-CE94-43D5-8FBA-0979331B06B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9bf20624e9921f92416c367634b9301d609d50c","datavalue":{"value":{"entity-type":"item","numeric-id":911773,"id":"Q911773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1332644$B17BD689-6BBA-416F-B4EF-3471C695D66F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb2c3f1d9cdf6d0af916eae57c1be76e6004b8b2","datavalue":{"value":{"entity-type":"item","numeric-id":3490986,"id":"Q3490986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c084dc58f1ed617014a49d377e67bae2876113fc","datavalue":{"value":{"amount":"+0.8075152039527893","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":"Q1332644$D234B424-E4E7-4A5F-949D-22A161C018D0","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":"aae17169631af7cd375db893af585b1aeb59cbb5","datavalue":{"value":{"amount":"+0.7901045083999634","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":"Q1332644$63632E91-26F6-4944-9D68-8343CA7FB96C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c920ed85419125dfdb595a601c3e525a0405742d","datavalue":{"value":{"entity-type":"item","numeric-id":4924965,"id":"Q4924965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3439f7e9798eb80eb908c2a5c77e55f724b2078a","datavalue":{"value":{"amount":"+0.7882220149040222","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":"Q1332644$FDAEF025-F202-4E07-9E41-27708B246738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c4ca972053202fcadf05af1326afd1b3c2d5c94","datavalue":{"value":{"entity-type":"item","numeric-id":4287499,"id":"Q4287499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"109c935fcf6e24d81c09a56f85edec4bc2e05c45","datavalue":{"value":{"amount":"+0.7753860950469971","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":"Q1332644$F880271E-B0EB-4FFB-AF93-6CAD8BECC9C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9db09a7fb68a35978bf8fa26d9ca51fa460cb0e7","datavalue":{"value":{"entity-type":"item","numeric-id":4450440,"id":"Q4450440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d62c08a0601b4b1d01469dbc738b703c1552b1ec","datavalue":{"value":{"amount":"+0.7692171335220337","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":"Q1332644$93AAF75A-D7D7-44A4-8164-3A59A85536F2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Resolution theorem proving in reified modal logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Resolution_theorem_proving_in_reified_modal_logics"}}}}}