MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Suda, Martin
Weidenbach, Christoph
dblp
dblp
Editor(s):
Bjørner, Nikolaj
Voronkov, Andrei
dblp
dblp
Not MPII Editor(s):
Bjørner, Nikolaj
Voronkov, Andrei
BibTeX cite key*:
SudaWeidenbachLPAR2012
Title, Booktitle
Title*:
Labelled Superposition for PLTL
Booktitle*:
Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18
Event, URLs
Conference URL::
http://www.cs.miami.edu/~geoff/Conferences/LPAR-18/
Downloading URL:
http://link.springer.com/content/pdf/10.1007%2F978-3-642-28717-6_31
Event Address*:
Mérida, Venezuela
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
11 March 2012
Event End Date:
15 March 2012
Publisher
Name*:
Springer
URL:
http://www.springer.com
Address*:
Berlin
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
7180
Number:
Month:
Pages:
391-405
Year*:
2012
VG Wort Pages:
ISBN/ISSN:
978-3-642-28716-9
Sequence Number:
DOI:
10.1007/978-3-642-28717-6_31
Note, Abstract, ©
(LaTeX) Abstract:
This paper introduces a new decision procedure for PLTL based on labelled superposition.
Its main idea is to treat temporal formulas as infinite sets of purely propositional clauses over an extended signature. These infinite sets are then represented by finite sets of labelled propositional clauses. The new representation enables the replacement of the complex temporal resolution rule, suggested by existing resolution calculi for PLTL, by a fine grained repetition check of finitely saturated labelled clause sets followed by a simple inference. The completeness argument is based on the standard model building idea from superposition. It inherently justifies ordering restrictions, redundancy elimination and effective partial model building. The latter can be directly used to effectively generate counterexamples of non-valid PLTL conjectures out of saturated labelled clause sets in a straightforward way.
Keywords:
Propositional Linear Temporal Logic, Superposition, Decision Procedure
HyperLinks / References / URLs:
http://www.mpi-inf.mpg.de/~suda/supLTL.html
Download
Access Level:
Internal

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{SudaWeidenbachLPAR2012,
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
EDITOR = {Bjørner, Nikolaj and Voronkov, Andrei},
TITLE = {Labelled Superposition for {PLTL}},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18},
PUBLISHER = {Springer},
YEAR = {2012},
VOLUME = {7180},
PAGES = {391--405},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Mérida, Venezuela},
ISBN = {978-3-642-28716-9},
DOI = {10.1007/978-3-642-28717-6_31},
}


Entry last modified by Anja Becker, 03/07/2013
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
12/11/2012 11:00:08 AM
Revisions
2.
1.
0.

Editor(s)
Anja Becker
Martin Suda
Martin Suda

Edit Dates
07.03.2013 14:46:34
08.02.2013 11:28:51
12/11/2012 11:00:08 AM