Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 DetailsÜbersicht
  Superposition Modulo Non-linear Arithmetic

Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., & Weidenbach, C. (2011). Superposition Modulo Non-linear Arithmetic. In V. Sofronie-Stokkermans, & C. Tinelli (Eds.), Frontiers of Combining Systems (pp. 119-134). Berlin: Springer. doi:10.1007/978-3-642-24364-6_9.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-001A-1529-9 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-1DA2-9
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Eggers, Andreas1, Autor
Kruglov, Evgeny1, Autor
Kupferschmid, Stefan1, Autor
Scheibler, Karsten1, Autor
Teige, Teige1, Autor
Weidenbach, Christoph2, Autor           
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 20112011
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: KruglovFroCoS2011
DOI: 10.1007/978-3-642-24364-6_9
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 8th International Symposium on Frontiers of Combining Systems
Veranstaltungsort: Saarbruecken, Germany
Start-/Enddatum: 2011-10-05 - 2011-10-07

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Frontiers of Combining Systems
  Untertitel : 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings
  Kurztitel : FroCoS 2011
Genre der Quelle: Konferenzband
 Urheber:
Sofronie-Stokkermans, Viorica1, Herausgeber           
Tinelli, Cesare2, Herausgeber
Affiliations:
1 Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545            
2 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 119 - 134 Identifikator: ISBN: 978-3-642-24363-9

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
  Kurztitel : LNAI
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 6989 Artikelnummer: - Start- / Endseite: - Identifikator: -