A Tabulation Proof Procedure for First-order Residuated Logic Programs: Soundness, Completeness and Optimizations

Residuated logic programs have shown to be a generalisation of a number of approaches to logic programming under uncertain or vague information, including fuzzy or annotated or probabilistic or similarity-based logic programming frameworks. Various computational approaches have been developed for propositional residuated logic programs: on the one hand, there exists a bottom-up neural-like implementation of the fixed-point semantics which calculates the successive iterations of the immediate consequences operator; on the other hand, a goal-oriented top-down tabulation procedure has recently been introduced. In this paper, we introduce a sound and complete tabulation-based proof procedure for the first-order extension of residuated logic programs.