8 July 2019 - Juan Casanova

Abstract

Meta-resolution is the name of the algorithm that I have developed to find provable instantiations of formulas with meta-variables in first-order logic that minimizes the search space through least commitment approaches. The need to develop this algorithm came from performance problems in applying the framework for finding faults in logical ontologies based on fault patterns that I had considered previously, but it has quickly come to our attention that it may have many other applications.

Questions that I often hear about it is how its unification approach is related to higher order unification and whether we are sure that the problem cannot be solved in an easier way using existing automated theorem proving algorithms. For some time, my answers to these questions were based mostly on intuition and examples. I can now provide a better response: formulas with meta-variables are a particular case of second order logic formulas, but finding provable instantiations for them is not a particular case of second order theorem proving and, perhaps more importantly, restrictions in the second order elements that may appear in the formulas make meta-resolution able to reduce the search space considerably by exploiting these restrictions.

In the talk, I will briefly motivate and introduce meta-resolution in the context of my PhD, explain the notions described above and more importantly give an account of what meta-resolution is and why it is a good approach to this problem. This talk is part of my second year PhD review and as such I will describe the wide range of insights that I have gained over the last year about the problem that I am trying to solve and my approach to it.