DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2019.19

Simplifying Inductive Schemes in Temporal Logic

Authors: Pablo Cordero, Inmaculada Fortes, Inmaculada P. de Guzmán, and Sixto Sánchez

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.

Cite as

Pablo Cordero, Inmaculada Fortes, Inmaculada P. de Guzmán, and Sixto Sánchez. Simplifying Inductive Schemes in Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{cordero_et_al:LIPIcs.TIME.2019.19,
  author =	{Cordero, Pablo and Fortes, Inmaculada and de Guzm\'{a}n, Inmaculada P. and S\'{a}nchez, Sixto},
  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 =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.19},
  URN =		{urn:nbn:de:0030-drops-113773},
  doi =		{10.4230/LIPIcs.TIME.2019.19},
  annote =	{Keywords: Linear Temporal Logic, Inductive Schemes, Loop-check}
}

Search Results

Documents authored by Sánchez, Sixto

Simplifying Inductive Schemes in Temporal Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message