Abstract
Certain approaches to detecting faults in ontologies rely on the ability to obtain provable instantiations of schematic formulas containing meta-variables (variables ranging over sub-formulas). One way to obtain such instantiations is to solve systems of constraints over unifiers arising from a generalization of resolution. A system of constraints over unifiers is a set of equations including first-order logic terms and atoms, as well as unifier variables. Such a system is satisfied by a set of substitutions (one for each unifier variable) if the equations hold for those substitutions and if each substitution is the most general unifier for the equation of which it is the outer-most unifier. Without meta-variables, each well formed system has at most one solution, which can be obtained by the well known most general unifier algorithm. However, when a system includes meta-variables that give rise to different most general unifiers. We implemented an algorithm designed to solve systems with meta-variables, giving an enumeration of both most general unifiers and meta-variable instantiations in an efficient way.
| Original language | English |
|---|---|
| Pages | 4-5 |
| Number of pages | 2 |
| Publication status | Published - 13 Apr 2018 |
| Event | 25th Automated Reasoning Workshop 2018: Bridging the Gap between Theory and Practice - University of Cambridge, Cambridge, United Kingdom Duration: 12 Apr 2018 → 13 Apr 2018 https://www.cl.cam.ac.uk/events/arw2018/ |
Workshop
| Workshop | 25th Automated Reasoning Workshop 2018 |
|---|---|
| Abbreviated title | ARW 2018 |
| Country/Territory | United Kingdom |
| City | Cambridge |
| Period | 12/04/18 → 13/04/18 |
| Internet address |