| Logic programming began in the early 1970's as a direct outgrowth of earlier work in automated theorem proving and artificial intelligence. While much work has been done in the area of non-classical automated theorem proving, most current logic programming systems are still only applicable to classical logic as described, e.g., in Lloyd's “Foundations of Logic Programming” ([19]). The reason is that a non-classical logic programming system was believed inherently less efficient than the classical one and only few consideration has been given to the construction of such a system. In this thesis, a non-classical logic programming framework will be built on the basis of Stachinak's theories of resolution proof systems ([38]) and of knowledge representational formalism of definite formulas ([39]). A definite formula is a non-clausal analogue of a Horn clause and can be defined for classical logic and various non-classical logics (e.g., the n-valued Łukasiewicz logic). “Definite formulas are intrinsically non-clausal, but at the same time retain the syntactic flavor and algorithmic advantages of Horn Clauses” (cf. [39]). In this thesis, I demonstrate how to combine both of these theories to construct a general non-classical logic programming framework for resolution logics. |
