PVS Embeddings of Propositional and Quantified Modal Logic

• URL: http://arxiv.org/abs/2205.06391v1
• Date: Thu, 12 May 2022 22:44:29 GMT
• Title: PVS Embeddings of Propositional and Quantified Modal Logic
• Authors: John Rushby
• Abstract summary: This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Modal logics allow reasoning about various modes of truth: for example, what it means for something to be possibly true, or to know that something is true as opposed to merely believing it. This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic, while providing effective automation. The report introduces and formally specifies and verifies several standard topics in modal logic such as relationships between the standard modal axioms and properties of the accessibility relation, and attributes of the Barcan Formula and its converse in both constant and varying domains.

Related papers

• Modal Logic for Stratified Becoming: Actualization Beyond Possible Worlds [55.2480439325792]
  This article develops a novel framework for modal logic based on the idea of stratified actualization.<n>Traditional Kripke semantics treat modal operators as quantification over fully determinate alternatives.<n>We propose a system Stratified Actualization Logic (SAL) in which modalities are indexed by levels of ontological stability, interpreted as admissibility.
  arXiv  Detail & Related papers  (2025-06-12T18:35:01Z)
• Learning to Reason via Mixture-of-Thought for Logical Reasoning [56.24256916896427]
  Mixture-of-Thought (MoT) is a framework that enables LLMs to reason across three complementary modalities: natural language, code, and truth-table.<n>MoT adopts a two-phase design: (1) self-evolving MoT training, which jointly learns from filtered, self-generated rationales across modalities; and (2) MoT inference, which fully leverages the synergy of three modalities to produce better predictions.
  arXiv  Detail & Related papers  (2025-05-21T17:59:54Z)
• 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)
• Faithful Logic Embeddings in HOL -- Deep and Shallow [0.0]
  This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic.<n>The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic.
  arXiv  Detail & Related papers  (2025-02-26T17:08:07Z)
• LogiDynamics: Unraveling the Dynamics of Logical Inference in Large Language Model Reasoning [49.58786377307728]
  This paper adopts an exploratory approach by introducing a controlled evaluation environment for analogical reasoning. We analyze the comparative dynamics of inductive, abductive, and deductive inference pipelines. We investigate advanced paradigms such as hypothesis selection, verification, and refinement, revealing their potential to scale up logical inference.
  arXiv  Detail & Related papers  (2025-02-16T15:54:53Z)
• A Note on an Inferentialist Approach to Resource Semantics [48.65926948745294]
  'Inferentialism' is the view that meaning is given in terms of inferential behaviour. This paper shows how 'inferentialism' enables a versatile and expressive framework for resource semantics.
  arXiv  Detail & Related papers  (2024-05-10T14:13:21Z)
• Logic Agent: Enhancing Validity with Logic Rule Invocation [24.815341366820753]
  Chain-of-Thought prompting has emerged as a pivotal technique for augmenting the inferential capabilities of language models during reasoning tasks. This paper introduces the Logic Agent (LA), an agent-based framework aimed at enhancing the validity of reasoning processes in Large Language Models.
  arXiv  Detail & Related papers  (2024-04-28T10:02:28Z)
• Inferentialist Resource Semantics [48.65926948745294]
  This paper shows how inferentialism enables a versatile and expressive framework for resource semantics. How inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications. This integration enables reasoning about shared and separated resources in intuitive and familiar ways.
  arXiv  Detail & Related papers  (2024-02-14T14:54:36Z)
• 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)
• 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)
• Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
  This article presents a semantical embedding for public announcement logic with relativized common knowledge. It enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. The work constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology.
  arXiv  Detail & Related papers  (2021-11-02T15:14:52Z)
• Public Announcement Logic in HOL [0.0]
  shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic.
  arXiv  Detail & Related papers  (2020-10-02T06:46:02Z)
• Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
  We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic. Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic.
  arXiv  Detail & Related papers  (2020-08-06T02:13:11Z)

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.