Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2013) | last year (2012) | two years ago (2011) | Notes URL

Action:

login to update
Options:








Author, Editor

Author(s):

Eggers, Andreas
Kruglov, Evgeny
Kupferschmid, Stefan
Scheibler, Karsten
Teige, Teige
Weidenbach, Christoph
dblp
dblp
dblp
dblp
dblp
dblp
Not MPG Author(s):

Eggers, Andreas
Kupferschmid, Stefan
Scheibler, Karsten
Teige, Teige

Editor(s):

Sofronie-Stokkermans, Viorica
Tinelli, Cesare
dblp
dblp
Not MPII Editor(s):

Tinelli, Cesare

BibTeX cite key*:

KruglovFroCoS2011

Title, Booktitle

Title*:

SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic

Booktitle*:

8th International Symposium on Frontiers of Combining Systems

Event, URLs

URL of the conference:

http://www.mpi-inf.mpg.de/conferences/frocos2011/

URL for downloading the paper:


Event Address*:

Saarbruecken, Germany
Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

5 October 2011
Event End Date:

7 October 2011

Publisher

Name*:

Springer

URL:

http://www.springer.com

Address*:

Heidelberg
Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

6989
Number:


Month:


Pages:

119-134

Year*:

2011
VG Wort Pages:


ISBN/ISSN:

978-3-642-24363-9
Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

The first-order theory over non-linear arithmetic
including transcendental functions (NLA) is undecidable.
Nevertheless, in this paper we show that a particular combination
with superposition leads to a sound and complete calculus that
is useful in practice. We follow basically the ideas
of the SUP(LA) combination, but have to take care
of undecidability, resulting in ``unknown'' answers by
the NLA reasoning procedure. A pipeline
of NLA constraint simplification techniques related to
the SUP(NLA) framework significantly decreases the number of ``unknown'' answers.
The resulting approach is implemented as SUP(NLA) by a system combination
of SPASS and iSAT. Applied to various scenarios
of traffic collision avoidance protocols, we show by experiments
that SPASS(iSAT) can fully automatically proof and disproof safety
properties of such protocols using the very same formalization.



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{KruglovFroCoS2011,
AUTHOR = {Eggers, Andreas and Kruglov, Evgeny and Kupferschmid, Stefan and Scheibler, Karsten and Teige, Teige and Weidenbach, Christoph},
 EDITOR = {Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
 TITLE = {{SUP(NLA)} -- Combining Superposition and Non-Linear Arithmetic},
 BOOKTITLE = {8th International Symposium on Frontiers of Combining Systems},
 PUBLISHER = {Springer},
 YEAR = {2011},
 VOLUME = {6989},
 PAGES = {119--134},
 SERIES = {Lecture Notes in Artificial Intelligence},
 ADDRESS = {Saarbruecken, Germany},
 ISBN = {978-3-642-24363-9},
}

Entry last modified by Evgeny Kruglov, 06/08/2012
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Attachment SectionAttachment Section