Labelled Superposition for PLTL

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Labelled Superposition for PLTL

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Labelled Superposition for PLTL

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

7180

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

15

Strana od-do

391-405

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—