English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 DetailsSummary
  Automatic Generation of Invariants for Circular Derivations in SUP(LA)

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.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-B7F8-D Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-03D3-E
Genre: Conference Paper
Latex : Automatic Generation of Invariants for Circular Derivations in {SUP(LA)}

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Fietzke, Arnaud1, Author           
Kruglov, Evgeny1, Author           
Weidenbach, Christoph1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2012
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: DOI: 10.1007/978-3-642-28717-6_17
BibTex Citekey: FietzkeKruglovWeidenbach2012a
Other: Local-ID: 97F000051AE9CBD9C12579FB003F6F27-FietzkeKruglovWeidenbach2012
 Degree: -

Event

show
hide
Title: 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Place of Event: Mérida, Venezuela
Start-/End Date: 2012-03-11 - 2012-03-15

Legal Case

show

Project information

show

Source 1

show
hide
Title: Logic for Programming, Artificial Intelligence, and Reasoning
  Subtitle : 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings
  Abbreviation : LPAR 2012
Source Genre: Proceedings
 Creator(s):
Bjørner, Nikolaj1, Editor
Voronkov, Andrei1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 197 - 211 Identifier: ISBN: 978-3-642-28716-9

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 7180 Sequence Number: - Start / End Page: - Identifier: ISSN: 0302-9743