The Annual SUMO Reasoning Prizes at CASC

[Home | Browse | Download | Publications | Tools | About]

Congratulations to the 2011 Winners! (at CASC-23)
    Proof and Assurance classes:
    • 1st: Vampire-LTB 1.8 - $1500
    • 2nd: iProver-SInE 0.9 - $1000
    • 3rd: E-LTB 1.4pre - $500
There were two articles written about the conference by the local Polish paper (courtesy of Google translate 1 2).

In summary, "easy" problems that were being solved in 2007 took three minutes to compute. Much harder problems, performing inference over the entire SUMO ontology, are now being solved in around 3 seconds.

The SUMO reasoning prize is for the best reasoning performance on a set of SUMO-based tests.

The SUMO inference prizes totalling US$3000.00 were awarded to the best performance on the SMO category of the LTB division of CASC, held as CADE each year. The LTB division has an assurance ranking class and a proof ranking class. In each ranking class the first place winner received $750, the second place $500, and the third place $250 (a system that wins the proof ranking class might also win the assurance ranking class).

Employees of the sponsor, its subcontractors and funded partners are not eligible. Submission of open source provers is encouraged, although not strictly required.

Full requirements and rules

Previous Year's Winners

2010 Winners: (at CASC-J5)

    Assurance class:
    • 1st: iProver
    • 2nd: Vampire-LTB 11.0
    • 3rd: Currahee

2009 Winners: (at CASC-22)

    Assurance class:
    • 1st: SInE-LTB 0.4
    • 2nd: iProver-SInE 0.7
    • 3rd: Vampire-LTB 11.0

2008 Winners: (at CASC-J4)

  • 1st (both classes) $1500 - SInE 0.3 - Krystof Hoder
  • 2nd (both classes) $1000 - MaLARea 0.3 - Josef Urban
  • 3rd (assurance class) $250 - iProver 0.5 - Konstantin Korovin
  • 3rd (proof class) $250 - Vampire 10.0 - Andrei Voronkov

The Suggested Upper Merged Ontology is a formal theory, like a dictionary for computers to read, of terms and logical definitions describing the world.

Reasoning on SUMO means answering a question, much like a database query. In contrast to a web search, which finds a likely answer in text that has already been written, reasoning means combining many small bits of information to compute an answer that has not been previously written, and then reporting the information used and how it was combined to deduce the answer.

Webmaster