Normative Conditional Reasoning as a Fragment of HOL

• URL: http://arxiv.org/abs/2308.10686v4
• Date: Sun, 7 Jul 2024 14:51:25 GMT
• Title: Normative Conditional Reasoning as a Fragment of HOL
• Authors: Xavier Parent, Christoph Benzmüller,
• Abstract summary: We discuss the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. We consider two possible uses of the framework.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The equivalence is automatically verified in one direction, leading from the property to the axiom. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox (or impossibility theorem) in population ethics, Parfit's repugnant conclusion. While some have proposed overcoming the impossibility theorem by abandoning the presupposed transitivity of ''better than'', our formalisation unveils a less extreme approach, suggesting among other things the option of weakening transitivity suitably rather than discarding it entirely. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.

Related papers

• (Quantum) Indifferentiability and Pre-Computation [50.06591179629447]
  Indifferentiability is a cryptographic paradigm for analyzing the security of ideal objects. Despite its strength, indifferentiability is not known to offer security against pre-processing attacks. We propose a strengthening of indifferentiability which is not only composable but also takes arbitrary pre-computation into account.
  arXiv  Detail & Related papers  (2024-10-22T00:41:47Z)
• Mitigating Misleading Chain-of-Thought Reasoning with Selective Filtering [59.495717939664246]
  Large language models have manifested remarkable capabilities by leveraging chain-of-thought (CoT) reasoning techniques to solve intricate questions. We propose a novel approach called the selective filtering reasoner (SelF-Reasoner) that assesses the entailment relationship between the question and the candidate reasoning chain. SelF-Reasoner improves the fine-tuned T5 baseline consistently over the ScienceQA, ECQA, and LastLetter tasks.
  arXiv  Detail & Related papers  (2024-03-28T06:28:35Z)
• Contrastive Chain-of-Thought Prompting [74.10511560147293]
  We propose contrastive chain of thought to enhance language model reasoning. Compared to the conventional chain of thought, our approach provides both valid and invalid reasoning demonstrations. Our experiments on reasoning benchmarks demonstrate that contrastive chain of thought can serve as a general enhancement of chain-of-thought prompting.
  arXiv  Detail & Related papers  (2023-11-15T18:54:01Z)
• Avoiding Pragmatic Oddity: A Bottom-up Defeasible Deontic Logic [1.160208922584163]
  This paper presents an extension of Defeasible Deontic Logic to deal with the Pragmatic Oddity problem. The logic applies three general principles: (1) the Pragmatic Oddity problem must be solved within a general logical treatment of CTD reasoning; (2) non-monotonic methods must be adopted to handle CTD reasoning; and (3) logical models of CTD reasoning must be computationally feasible and, if possible, efficient.
  arXiv  Detail & Related papers  (2022-09-09T23:14:09Z)
• Tree-Like Justification Systems are Consistent [0.0]
  Two variants of justification theory exist: one in which justifications are trees and one in which they are graphs. In this work we resolve the consistency problem once and for all for the tree-like setting by showing that all reasonable tree-like justification systems are consistent.
  arXiv  Detail & Related papers  (2022-08-05T10:48:08Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• A natural deduction system for orthomodular logic [0.0]
  Orthomodular logic is a weakening of quantum logic in the sense of Birkhoff and von Neumann. It is shown to be a nonlinear noncommutative logic. It is extended to two systems of predicate logic: the first is sound for Takeuti's quantum set theory, and the second is sound for a variant of Weaver's quantum logic.
  arXiv  Detail & Related papers  (2021-09-11T22:28:17Z)
• A Description Logic for Analogical Reasoning [28.259681405091666]
  We present a mechanism to infer plausible missing knowledge, which relies on reasoning by analogy. This is the first paper that studies analog reasoning within the setting of description logic.
  arXiv  Detail & Related papers  (2021-05-10T19:06:07Z)
• A Weaker Faithfulness Assumption based on Triple Interactions [89.59955143854556]
  We propose a weaker assumption that we call $2$-adjacency faithfulness. We propose a sound orientation rule for causal discovery that applies under weaker assumptions.
  arXiv  Detail & Related papers  (2020-10-27T13:04:08Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)

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.