Fuzzy relational calculi based on BK products of relations have representational and computational means for handling both concrete numerical representations of relations and symbolic manipulation of relations. BK calculus of relations together with fast fuzzy relational algorithms allows concrete numerical representations of relations to be used extensively in applications. On the other hand, when enriched by relational inequalities like BK Bootstrap or combined with other theories such as generalized morphisms, high level symbolic forms of relations can be used for symbolic manipulation of relations that have been abstracted from numerical representations. Furthermore, symbolic formulas of relations can be handled equationally. Equations over BK-products can characterize relational properties in a universal way.
The research in this dissertation focuses on symbolic manipulations of BK products of fuzzy relations. We have developed as a proof-of-concept an automated tool that works with various representational forms of relations and facilitates transformations among them. Major contribution that this system brings into the field is that, it provides a link between numerical and symbolic representations of relations, which can substantially extend the applicability of fuzzy relations.
The pilot implementation of the tool consists of two systems. At a high level of general fuzzy logic systems, the first system transforms BK-product formulas syntactically between three notational forms: matrix form, set form and predicate form. We have defined for each kind of BK-product representations a tree-type data structure, called a notational tree. All transformations are then carried out by set of transformational algorithms among the notational trees of BK representational forms.
At a lower level of t-norm based residuated logic systems (BL logic), we have developed a second system which is a term rewriting theorem prover/checker that validates and generates proofs for theorems of BK relational calculi. For each given theorem, a derivation tree will first be generated. A matching of any node in that tree with the theorem's conclusion will validate it. We proposed a generate-and-match algorithm based on a breadth-first-search navigation process through theorems' derivation trees which guarantees a loop-free result for any derivable theorem (in a given theory). The original version of this algorithm has been improved further by applying a human-like proof strategy, which we called distance-first-search and optimized distance-first-search algorithms. These optimized versions improve the performance of our system significantly, reducing both number of logical inferences and the CPU's time required. The experiments also showed that proofs in BK calculi are significantly shorter than in predicate calculus of BL logic. Interestingly enough, proofs generated by the tool are the same as those done by hand. This illustrates the successfulness of our human-like strategy.
