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):
Gramlich, Bernhard
Miller, Dale
Sattler, Uli
dblp
dblp
dblp
Not MPII Editor(s):
Gramlich, Bernhard
Miller, Dale
Sattler, Uli
BibTeX cite key*:
SudaWeidenbachIJCAR2012
Title, Booktitle
Title*:
A PLTL-prover based on labelled superposition with partial model guidance
Booktitle*:
Automated Reasoning : 6th International Joint Conference, IJCAR 2012
Event, URLs
Conference URL::
http://ijcar.cs.manchester.ac.uk/
Downloading URL:
http://link.springer.com/content/pdf/10.1007%2F978-3-642-31365-3_42
Event Address*:
Manchester, UK
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
26 June 2012
Event End Date:
29 June 2012
Publisher
Name*:
Springer
URL:
http://www.springer.com
Address*:
Berlin
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
7364
Number:
Month:
Pages:
537-543
Year*:
2012
VG Wort Pages:
ISBN/ISSN:
978-3-642-31364-6
Sequence Number:
DOI:
10.1007/978-3-642-31365-3_42
Note, Abstract, ©
(LaTeX) Abstract:
Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.
Keywords:
Propositional linear temporal logic (PLTL), Decision procedure, Resolution, Semantic guidance, Benchmarks
HyperLinks / References / URLs:
http://www.mpi-inf.mpg.de/~suda/ls4.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{SudaWeidenbachIJCAR2012,
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
EDITOR = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
TITLE = {A {PLTL}-prover based on labelled superposition with partial model guidance},
BOOKTITLE = {Automated Reasoning : 6th International Joint Conference, IJCAR 2012},
PUBLISHER = {Springer},
YEAR = {2012},
VOLUME = {7364},
PAGES = {537--543},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Manchester, UK},
ISBN = {978-3-642-31364-6},
DOI = {10.1007/978-3-642-31365-3_42},
}


Entry last modified by Anja Becker, 03/11/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:18:35 AM
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Anja Becker
Martin Suda
Martin Suda
Edit Dates
11.03.2013 14:10:41
07.03.2013 14:49:22
08.02.2013 11:29:21
12/11/2012 11:18:35 AM