Large theory reasoning with SUMO at CASC

Issue title: Practical Aspects of Automated Reasoning

Article type: Research Article

Authors: Pease, Adam | Sutcliffe, Geoff | Siegel, Nick | Trac, Steven

Affiliations: Articulate Software, USA. E-mails: {apease, nsiegel}@articulatesoftware.com | University of Miami, Miami, FL, USA. E-mails: {geoff, strac}@cs.miami.edu

Abstract: The Suggested Upper Merged Ontology (SUMO) has provided the TPTP problem library with problems that have large numbers of axioms, of which typically only a few are needed to prove any given conjecture. The LTB division of the CADE ATP System Competition tests the performance of ATP systems on these types of problems. The SUMO problems were used in the SMO category of the LTB division in 2008. This paper presents an analysis of the performance of the 2007 and 2008 CASC entrants on the SUMO problems, illustrating the improvements that can be achieved by various tuning techniques.

Keywords: Automated reasoning, large theories, commonsense reasoning

DOI: 10.3233/AIC-2010-0466

Journal: AI Communications, vol. 23, no. 2-3, pp. 137-144, 2010