IKL Reasoning Engine

Florida Institute For Human And Machine Cognition, Inc., Pensacola FL

Investigators

Abstract

Interoperation between systems which use extensive formalized knowledge is hampered by the wide variety of formalisms currently in use in such systems. Attempts to create World-wide Web standards have already yielded a collection of such formalisms, not all mutually compatible. This situation results in part from a methodology which views deductive efficiency of inference engines, rather than semantic clarity, as the primary design criterion for new formalisms. Recent work (reviving an older idea) has focussed instead on the design of a single, highly expressive, logic into which a wide number of existing formalisms can be straightforwardly mapped, essentially treating them as subsets or simple ontologies (theories) within the single common formalism. The resulting logic, called the Interoperation Knowledge Language (IKL), can express many representational strategies and the relationships between them in a single formalism, in principle overcoming this interoperation problem in many common cases. To realize this potential in practice requires an inference engine to process IKL. Although IKL is more expressive than first-order logic and so is not decidable, many of the formalisms translated into it have very tractable inference behavior. This project implements a new design of a reasoner which is theoretically complete for IKL, while also having the ability to recognize many of the known tractable subcases and use efficient inference strategies on inputs which fit into these known cases. The behavior of the engine is directed by scripts which control its search behavior in a highly flexible multi-directional search space combining hyper-resolution, rule-saturation and tableaux reasoning. The engine is designed as an experimental workbench rather than a production engine, with a focus on inventing useful techniques for controlling its behavior, running large experiment suites semi-automatically, and gathering information relevant to the search process. We plan to make use of this engine in a series of projects devoted to learning new inference strategies from empirical ontological data. Broader Impacts. The code created by this project will be publicly available under the GNU Lesser General Public Licence. Details of the project can be found on the project web page at http://homam.ihmc.us/silkie/Home.html