Using the tree representation of terms to recognize matching with neural networks Original Research Article

In this paper we investigate the use of neural networks to recognize the matching relation among First Order Logic (FOL) terms. Given n+1 terms {ti, T with i=1, …, n}, the network should identify those tis which are matched by T or one of its subterms. One of the main issues is how to properly represent the terms to be given as inputs to the networks. A way of mapping the tree structure of the terms into a form suitable to be input to a neural network is proposed. Results of experiments are presented in which some of the networks were able to recognize the matching relation in up to almost 95% of the cases. Finally “matchers” were built to solve sets of matching problems of the kind that often appear in rewriting based automated theorem proving. The results show a great reduction in the number of trials needed for solving such problems when using neural networks.