| Date: | 2015, February 24 (first talk) |
| Time: | |
| Author: | Kuksa, Eugen |
| Title: | Driving in the Rain and Eating Ice Cream – Do We Need This? Axiom Selection for Automated Theorem Proving |
Given large theories, automated theorem provers don't always choose the axioms to use for proving a conjecture wisely. Mostly only a handful of axioms is actually needed while dozens are supplied. This results in provers wasting resources on “useless” information and reaching their timeout before finding a proof. In this work, we develop and integrate axiom selection algorithms into Ontohub to speed up and even enable proving in those large theories.