The Boolean Solution Problem from the Perspective of Predicate Logic -- Extended Version

• URL: http://arxiv.org/abs/1706.08329v4
• Date: Wed, 02 Jul 2025 10:31:26 GMT
• Title: The Boolean Solution Problem from the Perspective of Predicate Logic -- Extended Version
• Authors: Christoph Wernhard,
• Abstract summary: Schr"oder investigated it as Aufl"osungsproblem (solution problem)<n>We show that it can be modeled on the basis of first-order logic extended by second-order predicate logic.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schr\"oder investigated it as Aufl\"osungsproblem (solution problem). It is closely related to the modern notion of Boolean unification. Today it is commonly presented in an algebraic setting, but seems potentially useful also in knowledge representation based on predicate logic. We show that it can be modeled on the basis of first-order logic extended by second-order quantification. A wealth of classical results transfers, foundations for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation become apparent. Although for first-order inputs the set of solutions is recursively enumerable, the development of constructive methods remains a challenge. We identify some cases that allow constructions, most of them based on Craig interpolation.

Related papers

• Interleaving Logic and Counting [5.71869130799784]
  Reasoning with quantifier expressions in natural language combines logical and arithmetical features.<n>Our topic is this cooperation of styles as it occurs in common linguistic usage.
  arXiv  Detail & Related papers  (2025-07-07T17:30:29Z)
• Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics [0.0]
  We develop forward chaining and normal form algorithms for reasoning about objects in cartesian categories with the rules for Horn logic.<n>We also adapt first-order unification to support multi-sorted theories, contexts, and fragments of first-order logic.
  arXiv  Detail & Related papers  (2025-04-27T18:02:02Z)
• Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework [93.59256448185954]
  We propose a logic-complete reasoning framework, Aristotle, with three key components: Logical Decomposer, Logical Search Router, and Logical Resolver.<n>In our framework, symbolic expressions and logical rules are comprehensively integrated into the entire reasoning process.<n>The experimental results on several datasets demonstrate that Aristotle consistently outperforms state-of-the-art reasoning frameworks in both accuracy and efficiency.
  arXiv  Detail & Related papers  (2024-12-22T10:14:09Z)
• Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning [28.111458981621105]
  Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short.<n>We propose a Compositional First-Order Logic Translation to capture logical semantics hidden in the natural language during translation.<n>We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches.
  arXiv  Detail & Related papers  (2024-10-10T15:42:39Z)
• Boolean Matching Reversible Circuits: Algorithm and Complexity [16.397487896227766]
  We show that the equivalence up to input negation and permutation is reversible in quantum time, while its classical complexity is exponential. This result is arguably the first demonstration of quantum exponential speedup in solving automation problems.
  arXiv  Detail & Related papers  (2024-04-18T13:47:17Z)
• Boolean Logic as an Error feedback mechanism [0.5439020425819]
  The notion of Boolean logic backpagation was introduced to build neural networks with weights and activations being Boolean numbers. Most of computations can be done with logic instead of real arithmetic during training and phases.
  arXiv  Detail & Related papers  (2024-01-29T18:56:21Z)
• Empower Nested Boolean Logic via Self-Supervised Curriculum Learning [67.46052028752327]
  We find that any pre-trained language models even including large language models only behave like a random selector in the face of multi-nested logic. To empower language models with this fundamental capability, this paper proposes a new self-supervised learning method textitCurriculum Logical Reasoning (textscClr)
  arXiv  Detail & Related papers  (2023-10-09T06:54:02Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols. We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
  arXiv  Detail & Related papers  (2023-06-29T18:35:41Z)
• Abstract Reasoning via Logic-guided Generation [65.92805601327649]
  Abstract reasoning, i.e., inferring complicated patterns from given observations, is a central building block of artificial general intelligence. This paper aims to design a framework for the latter approach and bridge the gap between artificial and human intelligence. We propose logic-guided generation (LoGe), a novel generative DNN framework that reduces abstract reasoning as an optimization problem in propositional logic.
  arXiv  Detail & Related papers  (2021-07-22T07:28:24Z)
• Logic Embeddings for Complex Query Answering [56.25151854231117]
  We propose Logic Embeddings, a new approach to embedding complex queries that uses Skolemisation to eliminate existential variables for efficient querying. We show that Logic Embeddings are competitively fast and accurate in query answering over large, incomplete knowledge graphs, outperform on negation queries, and in particular, provide improved modeling of answer uncertainty.
  arXiv  Detail & Related papers  (2021-02-28T07:52:37Z)
• 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.