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.<n>It provides a flexible verification framework based on the theories of dynamic logics.
• Score: 0.174048653626208
• License: http://creativecommons.org/licenses/by/4.0/
• 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

• On the Logical Content of Logic Programs [0.0]
  This paper introduces a novel perspective on Logic programming (LP) by defining a support'' relation that explicates what a program knows'' Results are formalized using the idea of base-extension semantics within proof-theoretic semantics. Our approach offers new insights into the logical foundations of LP and has potential applications in knowledge representation, automated reasoning, and formal verification.
  arXiv  Detail & Related papers  (2025-03-07T11:58:08Z)
• Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups [0.0]
  We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic. We outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
  arXiv  Detail & Related papers  (2025-02-26T10:10:10Z)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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.