Stephan Schulz
Automatische Theorembeweiser f¨r die Prädikatenlogik erster Stufe m¨ssen in der Regel in unendlichen Suchräumen nach Beweisen suchen. Die Steuerung dieser Suche erfolgt primär durch heuristische Evaluierungsfunktionen, die an wichtigen Verzweigungspunkten die verschiedenen Möglichkeiten bewerten. F¨r den Erfolg des Beweisers ist die Qualität dieser Bewertung von sehr hoher Bedeutung. Wir stellen ein Verfahren vor, das gute Evaluierungsfunktionen aus vielen früheren Beweiserfahrungen erlernt. Der Ansatz representiert Suchentscheidungen als Muster von Klauseln und erlernt Bewertungen durch Partitionierung des Raumes aller Muster. Der Ansatz wurde im Superpositionsbeweiser E/TSM implementiert und erfolgreich erprobt.