A resolution framework for finitely-valued first-order logics (Q1185455)

The authors outline a theoretical foundation for the introduction, analysis and implementation of resolution proof systems for finitely- valued first-order logics (FFO logics). They base their approach on the unification of the algebraic theories of logical systems and non-clausal resolution. Thus rich algebraic techniques should be at hand to express and investigate metatheoretical properties of resolution proof systems for FFO logics. First the notion of a resolution proof system for a first-order logic is introduced that generalizes the concept of a non-clausal resolution proof system for a propositional logic elaborated by the authors elsewhere and the resolution proof system for classical predicate logic developed by Manna and Waldinger. The proof that every FFO logics can be formalized as a resolution proof system entails the effective constructability of FFO resolution counterparts from the semantic descriptions of these logics. This sets the stage for an automated generation of theorem proving environments for FFO logics. At last two speed-up techniques, the set-of-support strategy and the polarity strategy, are examined to render the theorem proving system more effective. These techniques are to direct and restrict the application of the inference rules. It is demonstrated that both strategies preserve the refutational completeness of resolution proof systems.