Resolution approximation of first-order logics (Q1187026)

This paper is a continuation of other researches made by the author and P. O'Hearn in resolution proof systems. The idea behind this work is to represent a certain logic as a resolution-proof system. Of a certain interest are the strongly finite logics, that is, logics semantically defined by finite logical matrices. The main objective of the paper is to represent a logical system \(P\) not by a single resolution-proof system, but by a finite class of small proof systems \(K\), called the resolution approximation of \(P\). These systems can be run in parallel to determine if a given inference is valid in \(P\). This approach may offer a substantial saving of computing time. The main result of the paper establishes that for a strongly finite propositional logic \(P\) there exists a resolution approximation of \(P\). Moreover, there is an effective algorithm which constructs a minimal resolution approximation. The results are then extended to finitely- valued first-order logics.