Rasiowa-Sikorski deduction systems: A handy tool for computer science logics (Q4941933)

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].