RESOLUTION-BASED THEOREM-PROVING FOR MANY-VALUED LOGICS

A general approach to automated theorem proving for all first-order fi nite-valued logics that can be defined truth-functionally is described . The suggested proof procedure proceeds in two, largely independent, steps. First, logic-specific translation calculi are used to generate clause forms for arbitrary formulas of a many-valued logic. The worst- case complexity of the translation rules is analysed in some detail. I n the second step a simple resolution principle is applied to the logi c-free clause form. Some refinements of this resolution rule are demon strated to be refutationally complete by means of a generalized concep t of semantic trees. An investigation of some important families of ma ny-valued logics illustrates the concepts introduced by concrete examp les.