On Quantified Modal Theorem Proving for Modeling Ethics

• URL: http://arxiv.org/abs/1912.12959v1
• Date: Mon, 30 Dec 2019 15:14:21 GMT
• Title: On Quantified Modal Theorem Proving for Modeling Ethics
• Authors: Naveen Sundar Govindarajulu (Rensselaer AI and Reasoning Lab), Selmer Bringsjord (Rensselaer Polytechnic Institute), Matthew Peveler (Rensselaer Polytechnic Institute)
• Abstract summary: 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Meeting these requirements necessitates investigation of new approaches for proof automation. Particularly, a quantified modal logic, the deontic cognitive event calculus (DCEC), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DCEC, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.

Related papers

• On the Diagram of Thought [12.304069891580658]
  We introduce Diagram of Thought (DoT), a framework that models iterative reasoning in large language models (LLMs) DoT organizes propositions, critiques, refinements, and verifications into a cohesive DAG structure, allowing the model to explore complex reasoning pathways. We formalize the DoT framework using Topos Theory, providing a mathematical foundation that ensures logical consistency and soundness in the reasoning process.
  arXiv  Detail & Related papers  (2024-09-16T07:01:41Z)
• Understanding the differences in Foundation Models: Attention, State Space Models, and Recurrent Neural Networks [50.29356570858905]
  We introduce the Dynamical Systems Framework (DSF), which allows a principled investigation of all these architectures in a common representation. We provide principled comparisons between softmax attention and other model classes, discussing the theoretical conditions under which softmax attention can be approximated. This shows the DSF's potential to guide the systematic development of future more efficient and scalable foundation models.
  arXiv  Detail & Related papers  (2024-05-24T17:19:57Z)
• The Buffer Mechanism for Multi-Step Information Reasoning in Language Models [52.77133661679439]
  Investigating internal reasoning mechanisms of large language models can help us design better model architectures and training strategies. In this study, we constructed a symbolic dataset to investigate the mechanisms by which Transformer models employ vertical thinking strategy. We proposed a random matrix-based algorithm to enhance the model's reasoning ability, resulting in a 75% reduction in the training time required for the GPT-2 model.
  arXiv  Detail & Related papers  (2024-05-24T07:41:26Z)
• Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification [0.174048653626208]
  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.
  arXiv  Detail & Related papers  (2024-04-28T07:08:44Z)
• Applied Causal Inference Powered by ML and AI [54.88868165814996]
  The book presents ideas from classical structural equation models (SEMs) and their modern AI equivalent, directed acyclical graphs (DAGs) and structural causal models (SCMs) It covers Double/Debiased Machine Learning methods to do inference in such models using modern predictive tools.
  arXiv  Detail & Related papers  (2024-03-04T20:28:28Z)
• Automated legal reasoning with discretion to act using s(LAW) [0.294944680995069]
  ethical and legal concerns make it necessary for automated reasoners to justify in human-understandable terms. We propose to use s(CASP), a top-down execution model for predicate ASP, to model vague concepts following a set of patterns. We have implemented a framework, called s(LAW), to model, reason, and justify the applicable legislation and validate it by translating (and benchmarking) a representative use case.
  arXiv  Detail & Related papers  (2024-01-25T21:11:08Z)
• Learning Neural Constitutive Laws From Motion Observations for Generalizable PDE Dynamics [97.38308257547186]
  Many NN approaches learn an end-to-end model that implicitly models both the governing PDE and material models. We argue that the governing PDEs are often well-known and should be explicitly enforced rather than learned. We introduce a new framework termed "Neural Constitutive Laws" (NCLaw) which utilizes a network architecture that strictly guarantees standard priors.
  arXiv  Detail & Related papers  (2023-04-27T17:42:24Z)
• Dual Box Embeddings for the Description Logic EL++ [16.70961576041243]
  Similar to Knowledge Graphs (KGs), Knowledge Graphs are often incomplete, and maintaining and constructing them has proved challenging. Similar to KGs, a promising approach is to learn embeddings in a latent vector space, while additionally ensuring they adhere to the semantics of the underlying DL. We propose a novel ontology embedding method named Box$2$EL for the DL EL++, which represents both concepts and roles as boxes.
  arXiv  Detail & Related papers  (2023-01-26T14:13:37Z)
• Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming [8.677108656718824]
  Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks.
  arXiv  Detail & Related papers  (2021-06-28T10:43:25Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) The approach is underpinned by an inductive framework, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples. The outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine.
  arXiv  Detail & Related papers  (2020-07-07T07:39:42Z)
• A Simple Approach to Case-Based Reasoning in Knowledge Bases [56.661396189466664]
  We present a surprisingly simple yet accurate approach to reasoning in knowledge graphs (KGs) that requires emphno training, and is reminiscent of case-based reasoning in classical artificial intelligence (AI) Consider the task of finding a target entity given a source entity and a binary relation. Our non-parametric approach derives crisp logical rules for each query by finding multiple textitgraph path patterns that connect similar source entities through the given relation.
  arXiv  Detail & Related papers  (2020-06-25T06:28:09Z)

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.