2026-08-15T12:44:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11377 2024-03-06T10:48:04Z ddc:004 open_access

Simplifying Inductive Schemes in Temporal Logic Cordero, Pablo Fortes, Inmaculada de Guzmán, Inmaculada P. Sánchez, Sixto Linear Temporal Logic Inductive Schemes Loop-check 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pablo Cordero and Inmaculada Fortes and Inmaculada P. de Guzmán and Sixto Sánchez 2019 Is Part Of LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2019.19 urn:nbn:de:0030-drops-113773 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.19 eng https://creativecommons.org/licenses/by/3.0/legalcode