Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- URL: http://arxiv.org/abs/2404.18098v3
- Date: Wed, 7 Aug 2024 12:41:15 GMT
- Title: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- Authors: Yuanrui Zhang,
- Abstract summary: We propose a parameterized dynamic-logic-style' formalism, namely $DL_p$, for specifying and reasoning about general program models.
$DL_p$ provides a flexible verification framework to encompass different dynamic logic theories.
Case studies show how $DL_p$ works for reasoning about different types of program models.
- Score: 0.174048653626208
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Dynamic logic and its variations, because of their clear and expressive forms for capturing program properties, have been used as formalisms in program/system specification and verification for years and have many other applications. The program models of dynamic logics are in explicit forms. For different target program models, different dynamic logic theories have to be proposed to adapt different models' semantics. In this paper, we propose a parameterized `dynamic-logic-style' formalism, namely $DL_p$, for specifying and reasoning about general program models. In $DL_p$, program models and logical formulas are taken as `parameters', allowing arbitrary forms according to different interested domains. This characteristic allows $DL_p$ to support direct reasoning based on the operational semantics of program models, while still preserving compositional reasoning based on syntactic structures. $DL_p$ provides a flexible verification framework to encompass different dynamic logic theories. In addition, it also facilitates reasoning about program models whose semantics is not compositional, examples are neural networks, automata-based models, synchronous programming languages, etc. We mainly focus on building the theory of $DL_p$, including defining its syntax and semantics, building a proof system and constructing a cyclic preproof structure. We analyze and prove the soundness of $DL_p$. Case studies show how $DL_p$ works for reasoning about different types of program models.
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.