Thursday, March 17, 2011
Speaker: Krystof Hoder
Venue: TU Vienna
Reasoning with very large theories expressed in first-order logic canstrongly benefit from a good selection method for relevant axioms.This is confirmed by the fact that the largest available first-orderknowledge base (the Open CYC) contains over 3 million axioms, whileanswering queries to it usually requires not more than a few dozenaxioms.
A method for axiom selection has been proposed in the Sumo INferenceEngine (SInE) system. SInE has won the large theory division of CASCin 2008. The method turned out to be so successful that the next twoyears it was used by the winner of this division, as well as byseveral other competing systems. In this talk we will present thealgorithm and show experimental results based on its implementation inthe Vampire theorem prover.