License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2019.19
URN: urn:nbn:de:0030-drops-113773
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11377/
Go to the corresponding LIPIcs Volume Portal

Cordero, Pablo ; Fortes, Inmaculada ; de Guzmán, Inmaculada P. ; Sánchez, Sixto

Simplifying Inductive Schemes in Temporal Logic

pdf-format:
LIPIcs-TIME-2019-19.pdf (0.5 MB)

Abstract

In propositional temporal logic, the combination of the connectives "tomorrow" and "always in the future" require the use of induction tools. In this paper, we present a classification of inductive schemes for propositional linear temporal logic that allows the detection of loops in decision procedures. In the design of automatic theorem provers, these schemes are responsible for the searching of efficient solutions for the detection and management of loops. We study which of these schemes have a good behavior in order to give a set of reduction rules that allow us to compute these schemes efficiently and, therefore, be able to eliminate these loops. These reduction laws can be applied previously and during the execution of any automatic theorem prover. All the reductions introduced in this paper can be considered a part of the process for obtaining a normal form of a given formula.

BibTeX - Entry

@InProceedings{cordero_et_al:LIPIcs:2019:11377,
  author =	{Pablo Cordero and Inmaculada Fortes and Inmaculada P. de Guzm{\'a}n and Sixto S{\'a}nchez},
  title =	{{Simplifying Inductive Schemes in Temporal Logic}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{19:1--19:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11377},
  URN =		{urn:nbn:de:0030-drops-113773},
  doi =		{10.4230/LIPIcs.TIME.2019.19},
  annote =	{Keywords: Linear Temporal Logic, Inductive Schemes, Loop-check}
}

Keywords: Linear Temporal Logic, Inductive Schemes, Loop-check
Collection: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Issue Date: 2019
Date of publication: 07.10.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI