Reasoning about Intuitionistic Computation Tree Logic

• URL: http://arxiv.org/abs/2310.02355v1
• Date: Tue, 3 Oct 2023 18:30:39 GMT
• Title: Reasoning about Intuitionistic Computation Tree Logic
• Authors: Davide Catta, Vadim Malvone, Aniello Murano
• Abstract summary: 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.
• Score: 8.512802769278245
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this paper, we define an intuitionistic version of Computation Tree Logic. After explaining the semantic features of intuitionistic logic, we examine how these characteristics can be interesting for formal verification purposes. Subsequently, we define the syntax and semantics of our intuitionistic version of CTL and study some simple properties of the so obtained logic. We conclude by demonstrating that some fixed-point axioms of CTL are not valid in the intuitionistic version of CTL we have defined.

Related papers

• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures.
  arXiv  Detail & Related papers  (2024-05-03T16:38:14Z)
• Explaining Explanations in Probabilistic Logic Programming [0.0]
  In most approaches, the system is considered a black box, making it difficult to generate appropriate explanations. We consider a setting where models are transparent: probabilistic logic programming (PLP), a paradigm that combines logic programming for knowledge representation and probability to model uncertainty. We present in this paper an approach to explaining explanations which is based on defining a new query-driven inference mechanism for PLP where proofs are labeled with "choice expressions", a compact and easy to manipulate representation for sets of choices.
  arXiv  Detail & Related papers  (2024-01-30T14:27:37Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• Modeling Hierarchical Reasoning Chains by Linking Discourse Units and Key Phrases for Reading Comprehension [80.99865844249106]
  We propose a holistic graph network (HGN) which deals with context at both discourse level and word level, as the basis for logical reasoning. Specifically, node-level and type-level relations, which can be interpreted as bridges in the reasoning process, are modeled by a hierarchical interaction mechanism.
  arXiv  Detail & Related papers  (2023-06-21T07:34:27Z)
• The Lindstrom's Characterizability of Abstract Logic Systems for Analytic Structures Based on Measures [0.0]
  We extend Lindstrom's characterizability program to classes of infinitary logic systems. In particular, Hajek's Logic of Integral is redefined as an abstract logic with a new type of Hajek's satisfiability.
  arXiv  Detail & Related papers  (2023-02-26T21:48:25Z)
• Non-Deterministic Approximation Fixpoint Theory and Its Application in Disjunctive Logic Programming [11.215352918313577]
  Approximation fixpoint theory is a framework for studying the semantics of nonmonotonic logics. We extend AFT to dealing with non-deterministic constructs that allow to handle indefinite information. The applicability and usefulness of this generalization is illustrated in the context of disjunctive logic programming.
  arXiv  Detail & Related papers  (2022-11-30T18:58:32Z)
• Zero-Shot Classification by Logical Reasoning on Natural Language Explanations [56.42922904777717]
  We propose the framework CLORE (Classification by LOgical Reasoning on Explanations) CLORE parses explanations into logical structures and then explicitly reasons along thess structures on the input to produce a classification score. We also demonstrate that our framework can be extended to zero-shot classification on visual modality.
  arXiv  Detail & Related papers  (2022-11-07T01:05:11Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  Passage-level logical relations represent entailment or contradiction between propositional units (e.g., a concluding sentence) We propose logic structural-constraint modeling to solve the logical reasoning QA and introduce discourse-aware graph networks (DAGNs) The networks first construct logic graphs leveraging in-line discourse connectives and generic logic theories, then learn logic representations by end-to-end evolving the logic relations with an edge-reasoning mechanism and updating the graph features.
  arXiv  Detail & Related papers  (2022-07-04T14:38:49Z)
• Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective [1.160208922584163]
  Logic Programs with Ordered Disjunction (LPODs) extend classical logic programs with the capability of expressing preferential disjunctions. In this paper we obtain a purely logical characterization of strong equivalence of LPODs as logical equivalence in a four-valued logic. We provide a new proof of the coNP-completeness of strong equivalence for LPODs, which has an interest in its own right since it relies on the special structure of such programs.
  arXiv  Detail & Related papers  (2022-05-10T13:33:32Z)
• 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)
• Logical Neural Networks [51.46602187496816]
  We propose a novel framework seamlessly providing key properties of both neural nets (learning) and symbolic logic (knowledge and reasoning) Every neuron has a meaning as a component of a formula in a weighted real-valued logic, yielding a highly intepretable disentangled representation. Inference is omni rather than focused on predefined target variables, and corresponds to logical reasoning.
  arXiv  Detail & Related papers  (2020-06-23T16:55:45Z)

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.