Soundness and completeness of non-classical extended SLD-resolution

Abstract

We consider theoretical (mathematical) model of extended logic programming in many valued logic with arbitrary triple of connectives (seq, et1, et2), where et1 evaluates modus ponens containing the implication seq and et2 is the conjunction from bodies of clauses. Our motivation comes from MYCIN-like expert systems written in Prolog with uncertainty reasoning mechanism. Our declarative semantics is based on generalization of P. Hájek's RPL and RQL logic. We introduce a procedural semantics and prove soundness and completeness of this semantics for definite programs with confidence factors.