MPI-I-2012-RG1-001
Labelled superposition for PLTL
Suda, Martin and Weidenbach, Christoph
January 2012, 42 pages.
.
Status: available - back from printing
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.
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2012-RG1-001
BibTeX
@TECHREPORT{SudaWeidenbach2012,
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
TITLE = {Labelled superposition for {PLTL}},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-2012-RG1-001},
MONTH = {January},
YEAR = {2012},
ISSN = {0946-011X},
}