非表示:
キーワード:
-
要旨:
The success of superposition-based theorem proving in first-order logic relies
in particular on the fact that the superposition calculus can be turned into a
decision procedure for various decidable fragments of first-order logic and has
been successfully used to identify new decidable classes. In this paper, we
extend this story to the hierarchic combination of linear arithmetic and
first-order superposition. We show that decidability of reachability in timed
automata can be obtained by instantiation of an abstract termination result for
SUP(LA), the hierarchic combination of linear arithmetic and first-order
superposition.
