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
- The Stable Model Semantics for Higher-Order Logic Programming [4.106754434769354]
We propose a stable model semantics for higher-order logic programs.
Our semantics is developed using Approximation Fixpoint Theory (AFT), a powerful formalism.
We provide examples in different application domains, which demonstrate that higher-order logic programming under the stable model semantics is a powerful and versatile formalism.
arXiv Detail & Related papers (2024-08-20T06:03:52Z) - A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
We propose a unifying framework for modeling and analyzing multi-agent, knowledge-based, dynamic systems.
On the modeling side, we propose a process algebraic, agent-oriented specification language that makes such a framework easy to use for practical purposes.
arXiv Detail & Related papers (2024-07-24T08:35:50Z) - 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) - 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) - Language Model Cascades [72.18809575261498]
Repeated interactions at test-time with a single model, or the composition of multiple models together, further expands capabilities.
Cases with control flow and dynamic structure require techniques from probabilistic programming.
We formalize several existing techniques from this perspective, including scratchpads / chain of thought, verifiers, STaR, selection-inference, and tool use.
arXiv Detail & Related papers (2022-07-21T07:35:18Z) - 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) - Reactive Answer Set Programming [2.7286395031146062]
Logic Production System (LPS) is a logic-based framework for modelling reactive behaviour.
This paper proposes a systematic mapping of the Kernel of this framework (called KELPS) into an answer set program (ASP)
arXiv Detail & Related papers (2021-09-22T10:10:14Z) - A Logical Characterization of the Preferred Models of Logic Programs
with Ordered Disjunction [1.7403133838762446]
We provide a novel, model-theoretic semantics for Logic Programs with Ordered Disjunction (LPODs)
We demonstrate that the proposed approach overcomes the shortcomings of the traditional semantics of LPODs.
New approach can be used to define the semantics of a natural class of logic programs that can have both ordered and classical disjunctions in the heads of clauses.
arXiv Detail & Related papers (2021-08-07T05:36:12Z) - On Quantified Modal Theorem Proving for Modeling Ethics [0.0]
A quantified modal logic has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics.
We outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.
arXiv Detail & Related papers (2019-12-30T15:14: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.