Large theory reasoning with SUMO at CASC

Adam Pease, Geoff Sutcliffe, Nick Siegel, Steven Trac

Research output: Contribution to journalArticle

12 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)137-144
Number of pages8
JournalAI Communications
Volume23
Issue number2-3
DOIs
StatePublished - Apr 6 2010

Keywords

  • Automated reasoning
  • Commonsense reasoning
  • Large theories

ASJC Scopus subject areas

  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Large theory reasoning with SUMO at CASC'. Together they form a unique fingerprint.

  • Cite this