[Zurück]

G. Reger, M. Suda:
"When Should We Add Theory Axioms And Which Ones?";
Vortrag: 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl; 03.04.2016 - 07.04.2016.

One approach to first-order reasoning in the theory of arithmetic is to partially axiomatise the theory. For example, if an input problem uses the interpreted sum operation then one could add axioms stating that the operation is commutative and has identity zero. For obvious reasons it is not possible to add all necessary axioms. However, it may also be counter-productive to add all obvious axioms. For example, the commutativity axiom for sum is highly prolific in saturation-based methods and may not be necessary for solving the input problem. This talk presents a work-in-progress study applying machine learning to the problem of selecting which theory axioms to add given an input problem. The work is being carried out within the context of the Vampire theorem prover. The problem and the approach taken so far will be explained and some initial results given.

first-order theorem proving, theory reasoning, axiom selection

http://publik.tuwien.ac.at/files/publik_255096.pdf