Labelled Superposition for PLTL
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10125974" target="_blank" >RIV/00216208:11320/12:10125974 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/content/pdf/10.1007%2F978-3-642-28717-6_31" target="_blank" >http://link.springer.com/content/pdf/10.1007%2F978-3-642-28717-6_31</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-28717-6_31" target="_blank" >10.1007/978-3-642-28717-6_31</a>
Alternative languages
Result language
angličtina
Original language name
Labelled Superposition for PLTL
Original language description
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 byfinite 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.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Lecture Notes in Computer Science
ISSN
0302-9743
e-ISSN
—
Volume of the periodical
2012
Issue of the periodical within the volume
7180
Country of publishing house
DE - GERMANY
Number of pages
15
Pages from-to
391-405
UT code for WoS article
—
EID of the result in the Scopus database
—