Axiomsauswahl für automatische Beweissysteme

Automatische Beweissyteme haben in den vergangenen Jahren eine rasante Entwicklung durchlebt. Durch die Einbindung von Techniken des maschinellen Lernens konnten wirkungsvolle Heuristiken für die Beweisführung entwickelt werden. Dennoch führen große logische Theorien, wie sie in vielen Ontologien vorzufinden sind, oft zu Problemen. Daher erforschen wir in dieser Forschungsarbeit mögliche Ansätze des maschinellen Lernens, die es ermöglichen automatisiert jene Axiome aus einer großen Theorie auszuwählen, die gebraucht werden, um ein gegebenes Beweisziel zu erfüllen.