[Back]

G. Reger, M. Suda:
"Set of Support for Theory Reasoning";
Talk: IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana; 2017-05-07; in: "IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017", EasyChair Kalpa Publications in Computing, 1 (2017), 124 - 134.

This paper describes initial experiments using the set of support strategy to improve how a saturation-based theorem prover performs theory reasoning with explicit theory axioms.
When dealing with theories such as arithmetic, modern automated theorem provers often resort to adding explicit theory axioms, for example x+y = y+x. Reasoning with such axioms can be explosive. However, little has been done to explore methods that mitigate the negative impact of theory axioms on saturation-based reasoning.
The set of support strategy requires that all inferences
involve a premise with an ancestor in a so-called set of support,
initially taken to be a subset of the input clauses, usually those corresponding to the goal.
This leads to completely goal orientated reasoning but is, in general, incomplete.
The idea of this paper is to apply the set of support strategy to theory axioms only, and then to explore the effect of allowing some limited reasoning within this set.
The suggested approach is implemented and evaluated within the Vampire theorem prover.

automated theorem proving, theory reasoning, set of support, vampire

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