Axiom Selection in Commonsense Reasoning - Extension of the Hyper theorem prover[go to overview]
Subtasks within commonsense reasoning are the derivation of new information from existing knowledge (forward reasoning) and checking whether a statement (conjecture) can be derived from the given knowledge (backward reasoning). In order to perform the latter task, often a small subset of the knowledge is sufficient to prove the conjecture. The difficulty is to identify and select this subset in an automated way. Selection methods like SInE  and Similarity SInE  can be used to preselect knowledge that might be relevant. However, those methods do not always select enough or the right knowledge to find proof.
In my work, I want to expand the Hyper theorem prover so that a selection of knowledge is still possible during the proof procedure and not only as a preprocessing step. Afterward, possibilities will be evaluated and, in case of a positive result, implemented to support the selection of relevant knowledge through machine learning.
 K. Hoder and A. Voronkov. Sine qua non for large theory reasoning. In N. Bjørner and V. Sofronie-Stokkermans, editors, Automated Deduction – CADE-23, volume 6803 of Lecture Notes in Computer Science, pages 299–314. Springer Berlin Heidelberg, 2011.
 U. Furbach, T. Krämer, and C. Schon. Names are not just Sound and Smoke: Word Embeddings for Axiom Selection. Automated Deduction – CADE 27. CADE 2019
13.06.19 - 10:15