September 2019
EUSFLAT'19
13/09/19/11:28 Filed in: Conference participation
European Conference on Fuzzy Logic and Technology. Prague, September 9-13, 2019
We have attended the conference for presenting two papers, and participating in the Board Meeting of the journal Fuzzy Sets and Systems and the EUSFLAT General Assembly.
As usual, a good conference, very well-attended, with a friendly atmosphere which invites to meet a number of colleagues who work in our and related research topics.
In the picture above, the heads of Lluis Godo, Francesc Esteva and Irina Perfilieva attending our talks in the first seats.
Conference paper accepted
02/09/19/11:38 Filed in: Conference papers
P. Cordero, I. Fortes, I.P. de Guzmán and S. Sánchez. Simplifying Inductive Schemes in Temporal Logic. 26th Int Symp on Temporal Representation and Reasoning (TIME), Málaga, 2019.
ABSTRACT In propositional temporal logic, the combination of the connectives “tomorrow” and “always in the future” requires 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.
ABSTRACT In propositional temporal logic, the combination of the connectives “tomorrow” and “always in the future” requires 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.