Previous CASC competitions have focused on proving difficult problems on small numbers of axioms. However, typical reasoning applications for expert systems rely on knowledge bases that have large numbers of axioms of which only a small number may be relevant to any given query. We have created a category in the new LTB division of CASC to test this sort of situation. We present an analysis of performance of last year's entrants in CASC to show how they perform before any opportunity for tuning them to this new competition.
We created an additional test to support the participation of modelfinders. The SUMO validation prize totaling US$300 will test these systems, and hopefully improve SUMO by finding any problems with the theory. Three subdivisions, each with a $100 prize will be given to those systems which 1. Verify the consistency of, or provide feedback to repair, the base SUMO ontology. 2. Verify the consistency of, or provide feedback to repair, the combined SUMO and MILO ontologies. 3. Verify the consistency of, or provide feedback to repair, the combined SUMO, MILO, and domain ontologies. The winners of the SUMO challenges will be announced and receive their awards at IJCAR following successful completion of a challenge. 3.Example Test To give a flavor of what the tests consist of, we present one of them. The question posed to the system can be described as “Can a human perform an intentional action if he or she is dead?”. We create in the test an example instance of an action (instance DoingSomething4-1 IntentionalProcess) then state that an individual is performing the action (agent DoingSomething4-1 Entity4-1) and that the individual is human (instance Entity4-1 Human) The successful theorem prover will then find the following axioms and apply them to prove the conjecture (<=> (instance ?X4 Agent) (exists (?X5)
(agent ?X5 ?X4))) (subclass IntentionalProcess Process) (=> (and (subclass ?X403 ?X404) (instance ?X405 ?X403)) (instance ?X405 ?X404)) (=> (and (agent ?X5 ?X4) (instance ?X5 IntentionalProcess)) (and (instance ?X4 CognitiveAgent) (not (holdsDuring (WhenFn ?X5) (attribute ?X4 Dead))))) We should note that this proof has the interesting feature that although the form appears to be second order (holdsDuring arg <formula>), the system treats the embedded formula as an uninterpreted list and is able to solve the problem simply by unifying clauses in the list.
While this example is trivial when the necessary axioms are found ahead of time, it becomes very challenging in the context of a large knowledge base, where, in a practical situation, the relevant axioms cannot be known ahead of time. There are hundreds or thousands of axioms involving the term “agent” in SUMO, for example, and the successful theorem prover will have to hunt through those axioms very quickly in order to find just the ones that are relevant to the query being posed.
SNARK 20070805 Zenon 0.5.0
All Metis 2.0 Zenon 0.5.0
Overall performance is shown in the first column above with Vampire achieving first place. All other provers not listed failed to solve any of the problems. The best performance with SUMO alone is shown then SUMO+MILO and finally performance with all the domain ontologies loaded. The best performing provers still did not solve a majority of the 105 problems in the test set. Vampire solved 31, Fampire 20, E 15 and Metis 14, with the other provers in the single digits or no solutions at all. Prover failing to find solutions were stopped generally because of timeouts, rather than errors in parsing or memory space. Average running times approached the 600 seconds allocated for all provers because of the low percentage of solved problems.
The differing strengths of several of the provers suggested creating a “metaprover” combining several systems. The strategy is to give Vampire 400 seconds, then give Metis up to 200 seconds if Vampire failed to find a proof. The combined system gets 33 answers compared to 31 for Vampire alone or 14 for Metis alone, and performance overall is slightly better at 48158 seconds vs. 55419 for Metis and 48599 for Vampire. We might be able to tweak the timeslice allocation to do still better, although further efforts in that regard could be considered overtraining to this particular problem set.
We performed an analysis to determine what set of systems would cover the maximum number of problems (see Figure 1). This is termed a “SOTA” analysis as per (Sutcliffe & Suttner 2001). Vampire solved eight problems solved by no other prover. Metis uniquely solved two, and Fampire 1. This analysis suggests that we should revisit creation of a metaprover composed of Vampire, Metis and Fampire.
E
iProver
leanCoP
References Niles, I., and Pease, A. (2003) Linking Lexicons and Ontologies: Mapping WordNet to the Suggested Upper Merged Ontology, Proceedings of the IEEE International Conference on Information and Knowledge Engineering, pp 412416. Pease, A., (2004). Standard Upper Ontology Knowledge Interchange Format. Unpublished language manual. Available at http://sigmakee.sourceforge.net/ Scheffczyk, J., Pease, A., Ellsworth, M., (2006). Linking FrameNet to the Suggested Upper Merged Ontology, in Proceedings of Formal Ontology in Information Systems (FOIS2006), B. Bennett and C. Fellbaum, eds, IOS Press, pp 289300.
Sutcliffe G., Suttner C.B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2), 177203.