A G\"odel Calculus for Linear Temporal Logic
Juan Pablo Aguilera, Mart\'in Di\'eguez, David Fern\'andez-Duque,, Brett McLean
TL;DR
This paper introduces a deductive calculus for G"odel temporal logic, a fuzzy and superintuitionistic variant of linear temporal logic, establishing its soundness and completeness with respect to its semantics.
Contribution
It provides the first deductive calculus for G"odel temporal logic, linking its semantic properties to a formal proof system.
Findings
The calculus is sound for G"odel temporal logic.
The calculus is complete for G"odel temporal logic.
G"odel temporal logic is pspace}-complete.
Abstract
We consider G\"odel temporal logic (), a variant of linear temporal logic based on G\"odel--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 , and show this calculus to be sound and complete for the above-mentioned semantics.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems