On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI

• URL: http://arxiv.org/abs/2108.09876v1
• Date: Mon, 23 Aug 2021 00:42:22 GMT
• Title: On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI
• Authors: Adnan Darwiche and Pierre Marquis
• Abstract summary: We study the interplay between variable/literal and existential/universal quantification. We identify some classes of Boolean formulas and circuits on which quantification can be done efficiently.
• Score: 33.08556125025698
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification. We further identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former. This leads to a refinement of quantified Boolean logic with literal quantification as its primitive.

Related papers

• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations. We develop a quantum BI-style logic that includes interpretations for separating implication. We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
  arXiv  Detail & Related papers  (2024-09-16T10:34:45Z)
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs [6.2147758224415055]
  Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic.
  arXiv  Detail & Related papers  (2022-06-28T05:49:55Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs. In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
  arXiv  Detail & Related papers  (2022-05-04T08:57:44Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• Quantifying Qubit Magic Resource with Gottesman-Kitaev-Preskill Encoding [58.720142291102135]
  We define a resource measure for magic, the sought-after property in most fault-tolerant quantum computers. Our formulation is based on bosonic codes, well-studied tools in continuous-variable quantum computation.
  arXiv  Detail & Related papers  (2021-09-27T12:56:01Z)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  We propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. With novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs.
  arXiv  Detail & Related papers  (2020-08-15T23:56:18Z)
• 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)
• Logical Neural Networks [51.46602187496816]
  We propose a novel framework seamlessly providing key properties of both neural nets (learning) and symbolic logic (knowledge and reasoning) Every neuron has a meaning as a component of a formula in a weighted real-valued logic, yielding a highly intepretable disentangled representation. Inference is omni rather than focused on predefined target variables, and corresponds to logical reasoning.
  arXiv  Detail & Related papers  (2020-06-23T16:55:45Z)

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.