Intuitionistic Linear Temporal Logics

• URL: http://arxiv.org/abs/1912.12893v1
• Date: Mon, 30 Dec 2019 11:49:31 GMT
• Title: Intuitionistic Linear Temporal Logics
• Authors: Philippe Balbiani and Joseph Boudou and Mart\'in Di\'eguez and David Fern\'andez-Duque
• Abstract summary: We consider intuitionistic variants of linear temporal logic with next', until' and release' We prove that $iltl$ has the effective finite model property and hence is decidable, while $itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the until' and release' operators are not definable in terms of each other, even over the class of persistent posets.
• Score: 0.7087237546722617
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $\iltl$, and by imposing additional constraints we obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $\iltl$ has the effective finite model property and hence is decidable, while $\itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

Related papers

• Temporal Ensemble Logic [2.71467552808655]
  We introduce Temporal Ensemble Logic (TEL), a monadic, first-order modal logic for linear-time temporal reasoning. TEL has been motivated from the requirement for rigor and for cohort specification and discovery in clinical and population health research. We present its formal semantics, a proof system, and provide a proof for the satisfiability of the satisfiability of $rm TEL_mathbbN+$.
  arXiv  Detail & Related papers  (2024-08-26T17:36:25Z)
• Neuro-Symbolic Temporal Point Processes [13.72758658973969]
  We introduce a neural-symbolic rule induction framework within the temporal point process model. The negative log-likelihood is the loss that guides the learning, where the explanatory logic rules and their weights are learned end-to-end. Our approach showcases notable efficiency and accuracy across synthetic and real datasets.
  arXiv  Detail & Related papers  (2024-06-06T09:52:56Z)
• Reasoning about Intuitionistic Computation Tree Logic [8.512802769278245]
  We define an intuitionistic version of Computation Tree Logic. We demonstrate that some fixed-point axioms of CTL are not valid in the intuitionistic version of CTL.
  arXiv  Detail & Related papers  (2023-10-03T18:30:39Z)
• Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts [0.0]
  We focus on the extension of description logic $mathcalEL$. We show that for a useful fragment of the extension, the conclusions entailed by the different semantics coincide. For a slightly smaller, but still useful, fragment, we were also able to show decidability of the extension.
  arXiv  Detail & Related papers  (2023-08-16T09:37:38Z)
• Simulating Structural Plasticity of the Brain more Scalable than Expected [69.39201743340747]
  Rinke et al. introduced a scalable algorithm that simulates structural plasticity for up to one billion neurons on current hardware using a variant of the Barnes-Hut algorithm. We show that with careful consideration of the algorithm, the theoretical runtime can even be classified as $O(n log2 n)$.
  arXiv  Detail & Related papers  (2022-10-11T09:02:43Z)
• There is no Accuracy-Interpretability Tradeoff in Reinforcement Learning for Mazes [64.05903267230467]
  Interpretability is an essential building block for trustworthiness in reinforcement learning systems. We show that in certain cases, one can achieve policy interpretability while maintaining its optimality.
  arXiv  Detail & Related papers  (2022-06-09T04:23:26Z)
• Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
  We propose to understand logical symbols and expressions in the text to arrive at the answer. Based on such logical information, we put forward a context extension framework and a data augmentation algorithm. Our method achieves the state-of-the-art performance, and both logic-driven context extension framework and data augmentation algorithm can help improve the accuracy.
  arXiv  Detail & Related papers  (2021-05-08T10:09:36Z)
• Superposition with Lambdas [59.87497175616048]
  We design a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $betaeta$-equivalence classes of $lambda$-terms and rely on higher-order unification to achieve refutational completeness.
  arXiv  Detail & Related papers  (2021-01-31T13:53:17Z)
• Lexicographic Logic: a Many-valued Logic for Preference Representation [1.5484595752241122]
  We propose lexicographic logic, an extension of classical propositional logic that can express a variety of preferences. We argue that the new logic is an effective formalism for ranking query results according to the satisfaction level of user preferences.
  arXiv  Detail & Related papers  (2020-12-20T14:42:04Z)
• Thresholded Lasso Bandit [70.17389393497125]
  Thresholded Lasso bandit is an algorithm that estimates the vector defining the reward function as well as its sparse support. We establish non-asymptotic regret upper bounds scaling as $mathcalO( log d + sqrtT )$ in general, and as $mathcalO( log d + sqrtT )$ under the so-called margin condition.
  arXiv  Detail & Related papers  (2020-10-22T19:14:37Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  We introduce refutationally complete superposition calculi for intentional and extensional clausal $lambda$-free higher-order logic. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $lambda$-free higher-order lexicographic path and Knuth-Bendix orders.
  arXiv  Detail & Related papers  (2020-05-05T12:10:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.