Showing 1–4 of 4 results for author: Aguilera, J P

Gödel-Dummett linear temporal logic

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two… ▽ More We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This Gödel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that Gödel temporal logic is PSPACE-complete. We also provide a deductive calculus for Gödel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus. △ Less

Submitted 27 June, 2023; originally announced June 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2205.00574, arXiv:2205.05182

A Gödel Calculus for Linear Temporal Logic

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show thi… ▽ More We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics. △ Less

Submitted 10 May, 2022; originally announced May 2022.

Comments: arXiv admin note: text overlap with arXiv:2205.00574

Journal ref: Principles of Knowledge Representation and Reasoning, Proceedings of the 19th International Conference (August 2022) 2-11

Time and Gödel: Fuzzy temporal reasoning in PSPACE

Authors: Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean

Abstract: We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic do… ▽ More We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic does not have any form of the finite model property for these two semantics, we show that every falsifiable formula is falsifiable on a finite quasimodel, which yields decidability of the logic. We then strengthen this result by showing that this Gödel temporal logic is PSPACE-complete. △ Less

Submitted 1 May, 2022; originally announced May 2022.

Journal ref: Workshop on Logic, Language, Information, and Computation (WoLLIC), proceedings of the 28th International Workshop (September 2022), pp. 18-35

Unsound Inferences Make Proofs Shorter

Authors: Juan P. Aguilera, Matthias Baaz

Abstract: We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs. We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs. △ Less

Submitted 6 May, 2019; v1 submitted 27 August, 2016; originally announced August 2016.

Comments: 21 pages. July 2017 preprint

Journal ref: J. symb. log. 84 (2019) 102-122