Institute for Web Science and Technologies · Universität Koblenz - Landau

Axiom Selection in Commonsense Reasoning - Extension of the Hyper theorem prover

[go to overview]
Teresa Krämer

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 [1] and Similarity SInE [2] 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.

[1] 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.
[2] 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
B 016