On the Correctness of Symbolic Similarity-based Unfolding

Abstract

FASILL introduces “Fuzzy Aggregators and Similarity Into a Logic Language”. In its symbolic extension, called sFASILL, some truth degrees, similarity annotations, and fuzzy connectives can be left unknown, so that the user can easily figure out the impact of their possible values at execution time. We have recently formulated and implemented in a freely available online tool, a symbolic similarity-based variant of unfolding rule for sFASILL programs. This semantics-preserving transformation technique, very well known in most declarative frameworks, is based on the application of computational steps on the bodies of program rules for improving efficiency. In this paper, we formally prove the correctness of the transformation after adapting some safe applicability conditions previously used to safely unfold (non symbolic) FASILL programs.