{"entities":{"Q4941933":{"pageid":6971515,"ns":120,"title":"Item:Q4941933","lastrevid":108565472,"modified":"2026-11-07T00:21:51Z","type":"item","id":"Q4941933","labels":{"en":{"language":"en","value":"Rasiowa-Sikorski deduction systems: A handy tool for computer science logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1418370"}},"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":"Q4941933$1A2AD414-AC12-4008-A7C1-63BBF9A1B341","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"75f185c2071c9db2da0a82b13fabfe51b3b753aa","datavalue":{"value":"0949.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$D5A3E779-73C4-45DD-B7EF-C5D04917E85B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ffa73845da6faeb3595ac4dea6415bdc68ae4978","datavalue":{"value":{"entity-type":"item","numeric-id":229730,"id":"Q229730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4941933$654C234A-AECB-46AF-9D62-C73091993C3A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"990752c320d29232b9e0b8025fa1f119d1be577c","datavalue":{"value":{"time":"+2000-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4941933$9FF66CD1-DCA2-4A9E-8643-40D1F0A2C2ED","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25dae832a7b5192741ddf2b14ab8d2cca2e6e6a4","datavalue":{"value":"03B22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$043C873E-D333-4250-BDB7-833B6B52A8B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$D3635D3C-9DF6-4D49-9E56-F40E2C6DD095","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$D7A40C9C-C48B-472F-B044-8B67F0CEC25B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bf715f882d7ad0c07303aa3e6e3ac3725da52515","datavalue":{"value":"03B50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$0ABC8B3B-A6EF-483A-8ED6-A33E28B70FE7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1bfb0d2328691699f023b0cdf39b2f92cbd4e9ee","datavalue":{"value":"1418370","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$CDA86B7E-C26E-41B2-B36F-13D84731EAB7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$13F7E403-6A3B-435C-BC46-6FD3344808FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$F8F5F654-1249-40BD-B5C0-7ED82E7155A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5a0ff8c32958866c8802a26e0ad8674cbda54a8","datavalue":{"value":"three-valued logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$73F7C283-6646-40F9-A708-30F99609D738","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c7e2ecf1c1afaa0ef0cac38b590f4ca2866975e8","datavalue":{"value":"similarity","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$FA237C37-87BC-4352-9B5E-920E561E8D88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f532e2b08234dd6967fc70eafbf0c8f20a836d3e","datavalue":{"value":"nondeterminism","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$996161D4-D0AE-4E5C-AFA3-06878FE0E613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb0b691b2abb7641cf53161a75af650469af7e5c","datavalue":{"value":"Rasiowa-Sikorski deduction systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$A9696D4D-0541-4845-9515-8DB7DB12134C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f32defd18175082be6356fdfd3d64a8dd373b625","datavalue":{"value":"indiscernibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$167AFBDA-DEE9-43DF-BDF5-4AAC7EA652BC","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":"Q4941933$3A6EE2D5-0FFD-465B-8D2B-6E305D13BD5E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75a9fc31cce0a657eb9160065191d623889556e6","datavalue":{"value":{"entity-type":"item","numeric-id":1853457,"id":"Q1853457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99a702fbbfa7b94125c3f4a2a147a426b64bb1e9","datavalue":{"value":{"amount":"+0.8392477631568909","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":"Q4941933$C0201C88-5D02-4D4F-934D-B3D06C4F3EBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22e235861c01ffe98e9bc76be09360d0bff69eab","datavalue":{"value":{"entity-type":"item","numeric-id":2422312,"id":"Q2422312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8676f4937e49bc62e79cc29e6a0fa98eb10cbcc2","datavalue":{"value":{"amount":"+0.7869911193847656","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":"Q4941933$D4B0C314-5BA2-4932-8254-79668C6D7861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"908b2100e9fe9a88245b83919e1816b878373d70","datavalue":{"value":{"entity-type":"item","numeric-id":4267169,"id":"Q4267169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cfe39b8fa126f44dc145850fb735d11a76116586","datavalue":{"value":{"amount":"+0.7299452424049377","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":"Q4941933$C4CCB307-1732-4663-A5A4-05B420C3218E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3317123e5c3251d222b5f976bdb77838accc61e9","datavalue":{"value":{"entity-type":"item","numeric-id":3995436,"id":"Q3995436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bc40bf08b6bc4fad4be78380f2b8548c292c378","datavalue":{"value":{"amount":"+0.7292416095733643","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":"Q4941933$2A3CD566-03BE-4156-A4EB-2A10BA6AB644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5331b37b95be4ebbbb648e9bfd870d3a37599806","datavalue":{"value":{"entity-type":"item","numeric-id":1379289,"id":"Q1379289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aff9aa0da1ebd7efe10bdacdbebc4ae1a2582bd6","datavalue":{"value":{"amount":"+0.695732831954956","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":"Q4941933$B3129929-9C56-4F83-ACD9-4B091A8E19D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c8846107061e4d323dd67ab3f2c656b6b254136e","datavalue":{"value":{"text":"Rasiowa-Sikorski deduction systems: A handy tool for computer science logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4941933$F56D147D-20D3-4B14-B6B7-C5B048C68132","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"26f8c7d0cc0470e02ba804888609aaba63057fea","datavalue":{"value":"10.1007/3-540-48483-3_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4941933$F9233EFC-0D96-4ECE-8957-D803B564BEA7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4615dc466b71e856742d13de6248fccd71d32b2e","datavalue":{"value":"The paper provides a description of Rasiowa-Sikorski (R-S) deduction systems. The formalism of R-S deduction is a modification of the Gentzen natural-deduction system, i.e., it is in a sense dual to the well-known tableau method. Hence while in a tableau system we prove the validity of a formula \\(\\varphi\\) by showing that \\(\\neg\\varphi\\) is not satisfiable (has a closed tableau), in an R-S system we prove directly that \\(\\varphi\\) is (logically) valid (has a correct decomposition tree). R-S systems have proved to be a very convenient and powerful tool for developing proof mechanisms of various kinds of logics related to software specifications and knowledge representation. A notable feature of an R-S system is the fact that it is better suited to automation than a tableau method. The discussion is based on concrete examples coming from the author's experience connected with many-valued logics, nondeterminism, indiscernibility and similarity. A new result concerning a simple formalization of many-sorted first-order logic with possibly empty carriers of some sorts is given. The exposition is well structured and presented, but Theorem 1 (completeness) should be stated as follows: Any valid sequence of formulae is provable. For the entire collection see [Zbl 0921.00029].","type":"string"},"datatype":"string"},"type":"statement","id":"Q4941933$DB796039-4585-4C7B-BD9C-2F7392027C00","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4941933$F5C7E668-B9C6-4F6A-96D6-F562F60C6ED0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Rasiowa-Sikorski deduction systems: A handy tool for computer science logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Rasiowa-Sikorski_deduction_systems:_A_handy_tool_for_computer_science_logics"}}}}}