非表示:
キーワード:
-
要旨:
The hierarchic combination of linear arithmetic and firstorder
logic with free function symbols, FOL(LA), results in a strictly
more expressive logic than its two parts. The SUP(LA) calculus can be
turned into a decision procedure for interesting fragments of FOL(LA).
For example, reachability problems for timed automata can be decided
by SUP(LA) using an appropriate translation into FOL(LA). In this paper,
we extend the SUP(LA) calculus with an additional inference rule,
automatically generating inductive invariants from partial SUP(LA)
derivations. The rule enables decidability of more expressive fragments,
including reachability for timed automata with unbounded integer variables.
We have implemented the rule in the SPASS(LA) theorem prover
with promising results, showing that it can considerably speed up proof
search and enable termination of saturation for practically relevant
problems.
