DEDUCTION CHAINS AND DC-LIKE DECISION PROCEDURE FOR GUARDED LOGIC
Andrei Kouznetsov · 2004
The notion of Deduction Chain (DC) was suggested by K.Schütte to prove the completeness of first order logic (FOL). There is a question whether it is possible to provide the decision procedure for the guarded fragment of FOL (GF) on the basis of DC-rules. We propose here the decision procedure, or DCL algorithm, for the GF of FOL which rules are close to the ones of DC. DCL algorithm can be viewed as a ”mirrow ” of the tableau algorithm with the use of the so called blocking technique suggested in [4]. 1. Guarded Fragment The guarded fragment (GF) represents the special fragment of first-order logic (FOL), it was introduced by Andrèka, van Benthem, and Nèmeti [1.1], [1.2], and the main ideas go back to Nèmeti [5]. Let σ be a first-order relational structure (in which FO-formulas may contain symbols of arbitrary arity and constant symbols, but no function symbols of positive arity). The definition of the formula in GF is given as follows: