English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  DetailsSummary

Released
Conference Paper

Automatic Generation of Invariants for Circular Derivations in SUP(LA)

MPS-Authors
/persons/resource/persons44415

Fietzke,  Arnaud
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons44851

Kruglov,  Evgeny
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Fietzke, A., Kruglov, E., & Weidenbach, C. (2012). Automatic Generation of Invariants for Circular Derivations in SUP(LA). In N. Bjørner, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 197-211). Berlin: Springer.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B7F8-D
Abstract
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.