Deutsch
 
Benutzerhandbuch Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Superposition as a Decision Procedure for Timed Automata

MPG-Autoren
/persons/resource/persons44415

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

/persons/resource/persons45719

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Fietzke, A. L., & Weidenbach, C. (2013). Superposition as a Decision Procedure for Timed Automata. Mathematics in Computer Science, 6(4), 409-425. doi:10.1007/s11786-012-0134-5.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-B7C8-A
Zusammenfassung
The success of superposition-based theorem proving in first-order logic relies in particular on the fact that the superposition calculus can be turned into a decision procedure for various decidable fragments of first-order logic and has been successfully used to identify new decidable classes. In this paper, we extend this story to the hierarchic combination of linear arithmetic and first-order superposition. We show that decidability of reachability in timed automata can be obtained by instantiation of an abstract termination result for SUP(LA), the hierarchic combination of linear arithmetic and first-order superposition.