Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification

• URL: http://arxiv.org/abs/2404.18098v4
• Date: Wed, 29 Jan 2025 18:43:16 GMT
• Title: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
• Authors: Yuanrui Zhang,
• Abstract summary: We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models. It provides a flexible verification framework based on the theories of dynamic logics.
• Score: 0.174048653626208
• License:
• Abstract: We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models based on their transitional behaviours. Different from most dynamic logics that deal with regular expressions or a particular type of formalisms, DLp introduces a type of labels called "program configurations" as explicit program status for symbolic executions, allowing programs and formulas to be of arbitrary forms according to interested domains. This characteristic empowers dynamic logical formulas with a direct support of symbolic-execution-based reasoning, while still maintaining reasoning based on syntactic structures in traditional dynamic logics through a rule-lifting process. We propose a proof system and build a cyclic preproof structure special for DLp, which guarantees the soundness of infinite proof trees induced by symbolically executing programs with explicit/implicit loop structures. The soundness of DLp is formally analyzed and proved. DLp provides a flexible verification framework based on the theories of dynamic logics. It helps reduce the burden of developing different dynamic-logic theories for different programs, and save the additional transformations in the derivations of non-compositional programs. We give some examples of instantiations of DLp in particular domains, showing the potential and advantages of using DLp in practical usage.

Related papers

• 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)
• LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and Reasoning [73.98142349171552]
  LOGICSEG is a holistic visual semantic that integrates neural inductive learning and logic reasoning with both rich data and symbolic knowledge. During fuzzy logic-based continuous relaxation, logical formulae are grounded onto data and neural computational graphs, hence enabling logic-induced network training. These designs together make LOGICSEG a general and compact neural-logic machine that is readily integrated into existing segmentation models.
  arXiv  Detail & Related papers  (2023-09-24T05:43:19Z)
• 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)
• Argumentative Characterizations of (Extended) Disjunctive Logic Programs [2.055949720959582]
  We show that assumption-based argumentation can represent not only normal logic programs, but also disjunctive logic programs and their extensions. We consider some inference rules for disjunction that the core logic of the argumentation frameworks should respect.
  arXiv  Detail & Related papers  (2023-06-12T14:01:38Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)
• Logic of Differentiable Logics: Towards a Uniform Semantics of DL [1.1549572298362787]
  Differentiable logics (DLs) have been proposed as a method of training neural networks to satisfy logical specifications. This paper proposes a meta-language for defining DLs that we call the Logic of Differentiable Logics, or LDL. We use LDL to establish several theoretical properties of existing DLs, and to conduct their empirical study in neural network verification.
  arXiv  Detail & Related papers  (2023-03-19T13:03:51Z)
• 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)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
  arXiv  Detail & Related papers  (2021-10-18T10:45:59Z)
• Implementing Dynamic Answer Set Programming [0.0]
  We develop a translation of dynamic formulas into temporal logic programs. The reduction of dynamic formulas to temporal logic programs allows us to extend ASP with both approaches in a uniform way.
  arXiv  Detail & Related papers  (2020-02-17T12:34:14Z)

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.