Progress in Automating Higher-Order Ontology Reasoning
Christoph Benzmüller, Adam Pease · EPiC series in computing · 2018
We report on the application of higher-order automated theorem proving in ontology reasoning. Concretely, we have integrated the Sigma knowledge engineering environment and the Suggested Upper-Level Ontology SUMO with the higher-order theorem prover LEO-II. The basis for this integration is a translation from SUMO representations into the new typed higher-order form representation language TPTP THF. We illustrate the benefits of our integration with examples, report on experiments and analyze open challenges.