Introduction

The Knowledge Based Reasoning (KBR) community within the field of Artificial Intelligence has long conducted logical reasoning for decision support, planning and many similar applications [8]. Much of this has been done in the context of specialized logics and knowledge representation schemes, e.g., [10,6]. The Automated Theorem Proving (ATP) community has grown more out of mathematical disciplines, and its applications have tended to be in that realm using classical first-order logic, e.g., [4,1]. While the various uses of SNARK [20], e.g., [21,31], are notable exceptions, and several reasoning frameworks have been designed and implemented with a focus on large KBR, e.g., [17,11,29], there has not been a lot of use of general purpose classical ATP in KBR. This work brings together the KBR tool SigmaKEE and the ATP support of the TPTPWorld. The Sigma Knowledge Engineering Environment (SigmaKEE) [14] provides a mature platform for browsing and querying a knowledge base, often the Suggested Upper Merged Ontology (SUMO) [13]. The TPTPWorld provides well established standards, systems, and tools for first-order reasoning, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library [25]. While SigmaKEE has strong knowledge management features, it lacks the reasoning capabilities found in state of the art ATP systems. Conversely, while modern ATP systems are capable of proving hard theorems, they have limited features for interfacing with users of large knowledge bases. The integration of the TPTPWorld into SigmaKEE forms an interactive KBR environment, with strong knowledge management features, and access to modern state of the art ATP systems for reasoning over knowledge bases.

This paper is organized as follows: Sections 2 and 3 provide the necessary background about SigmaKEE and the TPTPWorld. Section 4 describes their integration, including extensions added to meet the needs of SigmaKEE users. Section 5 shows a sample use of the integrated system.

SigmaKEE

The Sigma Knowledge Engineering Environment (SigmaKEE) is a KBR environment for developing and using logical theories. It was created to support the Suggested Upper Merged Ontology (SUMO), which is written in a variant of the Knowledge Interchange Format (KIF) language [7] called Standard Upper Ontology Knowledge Interchange Format (SUO-KIF) [14]. SigmaKEE runs as an Apache Tomcat service, providing a browser interface to users. The main components are written in Java, and the user interface is generated by JSP. Users can upload a knowledge base for browsing and querying. An uploaded knowledge base is indexed for high performance browsing and searching. For ontology-like knowledge bases, which have a tree structure, a graph browser is provided. Figure 1 shows the graph browser interface for the top layers of the SUMO. Results from queries are presented in a hyperlinked KIF format that provides linkages back into the knowledge base, as shown in the example in Section 5.

The existing version of SigmaKEE includes a customized version of Vampire [18]. Among state of the art first order logical theorem provers available at the time of SigmaKEE's original development, only this version of Vampire, which is now 5 years old, had all the features required for theorem proving applications in SigmaKEE:

-The ability to extract an answer to a query as bindings of outermost existentially quantified variables in a conjecture. -The ability to generate a detailed proof that explains how an answer to a query was derived. -The ability to ask successive queries without reloading the knowledge base.

-The ability to perform basic arithmetic.

In addition, that version of Vampire was released under an approved open source license, and could therefore be tightly integrated with the open source SigmaKEE system.

TPTPWorld

The TPTPWorld is a package of TPTP data and software, including the TPTP problem library, a selection of ATP systems, and a suite of tools for processing TPTP format data. Although the TPTPWorld was developed and is primarily used for inhouse maintenance of the TPTP problem library, various components have become publically available and used in applications, e.g., [22,28].

One of the keys to the success of the TPTP and related projects is their consistent use of the TPTP language [23]. The TPTP language was designed to be suitable for writing both ATP problems and ATP solutions, to be flexible and extensible, and easily processed by both humans and computers. The TPTP language BNF is easy to translate into parser-generator (lex/yacc, antlr, etc.) input [30]. The SZS ontology [26] provides a fine grained ontology of result and output forms for ATP systems, so that their results can be precisely understood when used as input to other tools. The ontology also recommends the way that ontology values should be reported in the output from systems and tools. Figure 2 shows an extract from the top of the result ontology (the full ontology is available as part of the TPTP distribution).

The SystemOnTPTP utility is a harness that allows a problem written in the TPTP language to be easily and quickly submitted to a range of ATP systems and other tools. The implementation of SystemOnTPTP uses several subsidiary tools to prepare the input for the ATP system, control the execution of the chosen ATP system, and postprocess the output to produce an SZS result value and a TPTP format derivation. SystemOnTPTP runs in a UNIX environment, and is also available as an online service via http POST requests. 1The Interactive Derivation Viewer (IDV) [27] is a tool for graphical rendering and interaction with TPTP format derivations. The rendering uses shape and color to provide visual information about a derivation. The user can interact with the rendering in various ways -zooming, hiding, and displaying parts of the DAG according to various criteria, access to verification of the derivation, and an ability to provide a synopsis of a derivation by identifying interesting lemmas using AGInT [16]. Figure 3 shows the renderings of the derivation and synopsis for the proof output by EP [19] for the TPTP problem PUZ001+1.

The One Answer Extraction System (OAESys) and Multiple ANSwer EXtraction framework (MANSEX) are tools for question answering using ATP. Their development was motivated by the limited availability of modern ATP systems that are able to return answers -examples of systems that do are Otter [12], the 2 OAESys is a tool for extracting the bindings for outermost existentially quantified variables of a conjecture, from a TPTP format proof of the conjecture. This is done by reproving the conjecture using the Metis system [9], from only the axioms used in the original proof. The variable bindings that Metis reports for each inference step of its proof are analyzed to extract the required bindings (Metis is the only system that we know of that outputs TPTP format proofs and variable bindings for each inference step). The restriction to the axioms used in the original proof aims to make it unlikely for Metis to find a proof with different variable bindings from the original proof. If the axioms used are a subset of the axioms that were originally available, the problem given to Metis could be significantly easier than the original problem. MANSEX is a framework for interpreting a conjecture with outermost existentially quantified variables as a question, and extracting multiple answers to the question by repetitive calls to a system that can report the bindings for the variables in one proof of the conjecture. 3 Suitable systems for reporting bindings are an ATP system that outputs answers, e.g., SNARK, or a combination of an ATP system that outputs TPTP format proofs, e.g., EP, with OAESys. At each iteration of MANSEX, the conjecture is augmented by conjoining either inequalities or negative atoms that deny previously extracted answers. The ATP system is then called again to find a proof of the modified conjecture. In the SigmaKEE context the process has been extended to hide the conjecture modifications from the user -details are provided in Section 4. OAESys and MANSEX both use the proposed TPTP standards for question answering in ATP [24], and SNARK has also been adpated by its developer to use those standards.

The TPTP-parser is a highly reusable Java parser for TPTP data, built using the antlr parser-generator. 4 The parser can easily be used without modifications in practically any application. This universality is achieved by isolating the parser code by an interface layer that allows creation of and access to abstract syntax representations of various TPTP elements. A simple but reasonably efficient default implementation of the interface layer is provided with the package.

Integration of the TPTPWorld into SigmaKEE

The integration of the TPTPWorld provides SigmaKEE with new capabilities:

-Internal support for TPTP format problems and derivations, using a SUO-KIF to TPTP translation and the TPTP-parser. -Access to ATP systems for reasoning tasks, using SystemOnTPTP.

-Question answering using OAESys, with the ability to provide multiple answers through use of the MANSEX framework. -Presentation of TPTP format proofs using IDV, or using the existing hyperlinked KIF format extended with SZS ontology status values. -An extended browser interface for access to these capabilities.

The integration has been implemented by adding external TPTPWorld tools to the SigmaKEE distribution, and embedding Java implementations of TPTPWorld tools directly into SigmaKEE. SigmaKEE was developed to support knowledge bases written in SUO-KIF, e.g., SUMO. In order to make a large suite of ATP systems available for reasoning over such knowledge bases through use of the SystemOnTPTP utility, knowledge bases are translated to the TPTP language when they are loaded. While much of the translation is syntactic, there are some constructs in SUMO that require special processing [15]. These include use of sort signatures, sequence variables, variable predicates and functions, and embedded (higher-order) formulae.

Once a knowledge base has been loaded into SigmaKEE, queries can be submitted. A query is translated to a TPTP format conjecture, and the previously translated knowledge base provides the axioms. These are submitted to an ATP system through the SystemOnTPTP utility. Queries with outermost existentially quantified variables are treated as questions whose answers are the values bound to those variables in proofs. Three versions of SystemOnTPTP are available: remote access to the online SystemOnTPTP service via http POST requests, execution of a locally installed SystemOnTPTP, and a limited internal implementation of SystemOnTPTP. The ATP systems supported by the internal implementation are required to be TPTP-compliant in terms of both input and output, and have licensing that allows them to be added to SigmaKEE. At this stage E/EP, Metis, SNARK, and Paradox [5] are being used.

The advantage of using the local installation or internal implementation of SystemOnTPTP is that they do not rely on an online connection to the remote server. The advantage of the internal implementation is that it is portable to operating systems that do not have the UNIX environment required for Sys-temOnTPTP, e.g., Windows XP. The user chooses whether to use the remote SystemOnTPTP or a local one, and which ATP system to use. In the remote case the online system is queried to get a list of the available ATP systems. In the local case the ATP systems available in the local SystemOnTPTP installation (if any) and the internal implementation are available. If an ATP system is supported by the internal implementation and is also available through a local SystemOnTPTP installation, the internally supported one is used.

Answers to "question" conjectures are extracted from proofs using an embedding of OAESys into SigmaKEE. As Metis is one of the internally supported systems, it is available for use in OAESys. When the user requests more than one answer, an embedding of the MANSEX framework is used. In the SigmaKEE context the MANSEX process has been extended to displace the conjecture modifications from the user. This extension is done for the second and subsequent proofs found, as follows. After each answer has been extracted by OAESys, the existentially quantified variables in the original conjecture, i.e., the conjecture without the augmentations, are instantiated with the answer values. This instantiated conjecture and just the axioms used in the proof found by the chosen ATP system are passed to that ATP system. This additional ATP system run finds a proof of the (instantiated form of the) original conjecture, rather than of the augmented conjecture. Using MANSEX to get multiple answers is somewhat different, and can produce different answers, from using the customized version of Vampire mentioned in Section 2. MANSEX with OAESys requires multiple ATP system runs: two for the first answer (one to get a proof using the chosen ATP system and another to Metis within OAESys), and three for each successive answer (additionally the final call to the chosen ATP system). In contrast, the customized Vampire backtracks in its proof space to find multiple answers. As a side-effect, the customized Vampire can return the same answer multiple times if there are multiple proofs that produce the same variable bindings, while MANSEX does not.

The integration of the TPTPWorld provides SigmaKEE with three options for displaying results: TPTP format derivations in plain text format, IDV for displaying TPTP format derivations graphically, and the hyperlinked KIF format. IDV has been embedded into SigmaKEE so that it is directly available. The hyperlinked KIF format has been implemented by translation of TPTP format derivations into SUO-KIF using an augmentation of the TPTP-parser code, and then calling SigmaKEE's hyperlinked KIF presentation feature. The hyperlinked KIF format has been mildly extended to provide more precise information about the formulae in a proof, and to provide SZS status values. An example with a hyperlinked KIF format proof is given in Section 5.

The top part of Figure 5 shows the GUI interface. The interface allows the user to submit a query or to add to the current knowledge base. The interface has the following components (top to bottom, left to right):

-Formula text box -The query or additions are put into this text box in SUO-KIF format. -Local or Remote SystemOnTPTP, System -Choose which SystemOnTPTP to use, and which ATP system. -Maximum answers -Desired number of answers for the query.

-Query time limit -CPU time limit for the query.

-Output format -TPTP, IDV, or hyperlinked KIF -Ask button -Execute the ATP system on the query.

-Tell button -Add the data to the knowledge base.

Sample Use

As an example, EP's proof of the following SUO-KIF format query to the SUMO knowledge base is considered: (instance ?X PrimaryColor). The query asks for an instance of a primary color in the SUMO knowledge base. In SUMO the following are considered primary colors: Black, Blue, Red, White, and Yellow. The query was run using the internal implementation of SystemOnTPTP, asking for two answers, with a CPU limit of 300s, and hyperlinked KIF output. Figure 5 shows the result.

EP returns the first proof shown in the output, with SZS status Theorem. OAESys is used to extract the first answer -Red. The proof and answer are translated to the hyperlinked KIF format by SigmaKEE. MANSEX then augments the query to deny the answer Red, and EP returns another TPTP proof behind the scenes. OAESys is used to extract the second answer -Blue, which is used to instantiate the existentially quantified variable of the conjecture. EP returns the second proof shown in the output. The left column of the hyperlinked KIF is labeled SUO-KIF format formulae, with embedded HTML hyperlinks back to terms in the SUMO knowledge base. The right column describes the source of the formula: the parent formulae, the knowledge base (KB), or the query. While KBR and ATP are both mature fields, there has not been significant crossfertilization between the two communities. Both communities would benefit from a greater degree of interaction. The integration of the TPTPWorld into Sigma-KEE brings together tools that support both communities, which should make collaboration easier, and drive further cross-disciplinary research. The use of the remote SystemOnTPTP illustrates how KBR and other application systems can absolve themselves of the responsibility of maintaining up-to-date ATP systems in-house, and instead use an online service for discharging reasoning requests. The experience with SigmaKEE can be leveraged by others to this end.

Future work includes translation of SUMO and other knowledge bases to the new typed higher-order format (THF) of the TPTP language [3], and use of higher-order ATP systems such as LEO II [2] to answer higher-order queries over the knowledge bases.