Handbook of Automated Reasoning

6.3 Single step propositional systems

Single step rules corresponding to the free variable systems in the previous section have been introduced by Massacci [1994]. Massacci has given rules for a number of other systems as well; all of these logics have also been given a free variable formulation in [Beckert and Goré 1997].

Following the pattern used for intuitionistic logic in section 4.2I shall formulate a search procedure and use refutation trees to establish completeness. For the logics K4, KD4 and S4 the procedure implements a termination condition based on loop–checking. The loop–checking mechanism is defined by Fitting [1983] and has been investigated further by Demri [1995].

Loop–checking is computationally expensive. An alternative ...