Contradictions

• URL: http://arxiv.org/abs/2509.07026v1
• Date: Sun, 07 Sep 2025 13:47:51 GMT
• Title: Contradictions
• Authors: Yang Xu, Shuwei Chen, Xiaomei Zhong, Jun Liu, Xingxing He,
• Abstract summary: This paper focuses on the systematic construction of standard contradictions.<n>We propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction.<n>We derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction.
• Score: 9.602468627573215
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Trustworthy AI requires reasoning systems that are not only powerful but also transparent and reliable. Automated Theorem Proving (ATP) is central to formal reasoning, yet classical binary resolution remains limited, as each step involves only two clauses and eliminates at most two literals. To overcome this bottleneck, the concept of standard contradiction and the theory of contradiction-separation-based deduction were introduced in 2018. This paper advances that framework by focusing on the systematic construction of standard contradictions. Specially, this study investigates construction methods for two principal forms of standard contradiction: the maximum triangular standard contradiction and the triangular-type standard contradiction. Building on these structures, we propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction. Furthermore, we derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction. The results presented herein furnish the methodological basis for advancing contradiction-separation-based dynamic multi-clause automated deduction, thereby extending the expressive and deductive capabilities of automated reasoning systems beyond the classical binary paradigm.

Related papers

• Resolving Zadehs Paradox Axiomatic Possibility Theory as a Foundation for Reliable Artificial Intelligence [0.0]
  This work advances and substantiates the thesis that the resolution of this crisis lies in the domain of possibility theory.<n>The aim of this work is to demonstrate that possibility theory is not merely an alternative, but provides a fundamental resolution to DST paradoxes.
  arXiv  Detail & Related papers  (2025-12-04T21:13:16Z)
• On the Complexity of the Grounded Semantics for Infinite Argumentation Frameworks [0.0]
  We use methods from mathematical logic, specifically computability and set theory, to analyze the grounded extension.<n>Finding this fixed-point requires transfinite iterations.<n>This shows a marked distinction from the finite case where the grounded extension is-time computable.
  arXiv  Detail & Related papers  (2025-11-27T12:13:30Z)
• An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction [8.21204701022347]
  This paper proposes a novel automated theorem generation theory and tool.<n>It defines and proves, for the first time, a new logical structure known as rectangular standard contradiction.<n>To implement this theory, an efficient template-based ATG algorithm is designed.
  arXiv  Detail & Related papers  (2025-11-06T06:03:54Z)
• Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction [11.18154335347018]
  This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation.<n>By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning.
  arXiv  Detail & Related papers  (2025-10-12T17:03:33Z)
• Reasoning is about giving reasons [55.56111618153049]
  We show that we can identify and extract the logical structure of natural language arguments in three popular reasoning datasets with high accuracies.<n>Our approach supports all forms of reasoning that depend on the logical structure of the natural language argument.
  arXiv  Detail & Related papers  (2025-08-20T07:26:53Z)
• Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
  This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process is identical to the unique equilibrium of an unbounded revision dialogue between a system and its environment.<n>By unifying concepts from fixed point theory, game semantics, ordinal analysis, and type theory, this research establishes a broadly accessible yet formally rigorous foundation for reasoning about infinite self referential systems.
  arXiv  Detail & Related papers  (2025-07-25T13:12:55Z)
• Higher-Order Pattern Unification Modulo Similarity Relations [0.0]
  Combination of higher-order theories and fuzzy logic can be useful in decision-making tasks.<n>We adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaved components.<n>We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness.
  arXiv  Detail & Related papers  (2025-07-17T15:18:22Z)
• Soft Thinking: Unlocking the Reasoning Potential of LLMs in Continuous Concept Space [62.54887038032942]
  We introduce Soft Thinking, a training-free method that emulates human-like "soft" reasoning by generating soft, abstract concept tokens.<n>These concept tokens are created by the probability-weighted mixture of token embeddings, which form the continuous concept space.<n>In essence, each generated concept token encapsulates multiple meanings from related discrete tokens, implicitly exploring various reasoning paths to converge.
  arXiv  Detail & Related papers  (2025-05-21T17:29:15Z)
• Polynomial-Time Relational Probabilistic Inference in Open Universes [14.312814866832804]
  We introduce a method of first-order probabilistic inference that satisfies both the expressive power of the language used and the tractability of the computational problem posed by reasoning.<n> Specifically, we extend sum-of-squares logic of expectation to relational settings.<n>We are able to derive the tightest bounds provable by proofs of a given degree and size and establish completeness in our sum-of-squares refutations for fixed degrees.
  arXiv  Detail & Related papers  (2025-05-07T04:14:03Z)
• Fence Theorem: Towards Dual-Objective Semantic-Structure Isolation in Preprocessing Phase for 3D Anomaly Detection [32.44179060918441]
  Fence Theorem formalizing preprocessing as a dual-objective semantic isolator.<n>Patch3D, consisting of Patch-Cutting and Patch-Matching modules, to segment semantic spaces and consolidate similar ones.<n>Experiments on Anomaly-ShapeNet and Real3D-AD with different settings demonstrate that progressively finer-grained semantic alignment in preprocessing directly enhances point-level AD accuracy.
  arXiv  Detail & Related papers  (2025-03-03T01:58:11Z)
• Invariant Causal Set Covering Machines [48.169632766444906]
  Rule-based models, such as decision trees, appeal to practitioners due to their interpretable nature.<n>However, the learning algorithms that produce such models are often vulnerable to spurious associations and thus, they are not guaranteed to extract causally-relevant insights.<n>We propose Invariant Causal Set Covering Machines, an extension of the classical Set Covering Machine algorithm for conjunctions/disjunctions of binary-valued rules that provably avoids spurious associations.
  arXiv  Detail & Related papers  (2023-06-07T20:52:01Z)
• Understanding and Constructing Latent Modality Structures in Multi-modal Representation Learning [53.68371566336254]
  We argue that the key to better performance lies in meaningful latent modality structures instead of perfect modality alignment. Specifically, we design 1) a deep feature separation loss for intra-modality regularization; 2) a Brownian-bridge loss for inter-modality regularization; and 3) a geometric consistency loss for both intra- and inter-modality regularization.
  arXiv  Detail & Related papers  (2023-03-10T14:38:49Z)
• A contextually objective approach to the extended Wigner's friend thought experiment [0.0]
  We show that no contradiction arises if one admits that agents must agree on what is considered as a system and what is not. In such a contextually objective approach of quantum mechanics, the apparent contradiction is automatically removed.
  arXiv  Detail & Related papers  (2023-01-08T10:58:02Z)
• GroupifyVAE: from Group-based Definition to VAE-based Unsupervised Representation Disentanglement [91.9003001845855]
  VAE-based unsupervised disentanglement can not be achieved without introducing other inductive bias. We address VAE-based unsupervised disentanglement by leveraging the constraints derived from the Group Theory based definition as the non-probabilistic inductive bias. We train 1800 models covering the most prominent VAE-based models on five datasets to verify the effectiveness of our method.
  arXiv  Detail & Related papers  (2021-02-20T09:49:51Z)
• Tripartite Genuine Non-Gaussian Entanglement in Three-Mode Spontaneous Parametric Downconversion [56.12820031986851]
  We show that the states generated by a three-mode spontaneous parametric downconversion interaction Hamiltonian possess tripartite entanglement of a different nature to other paradigmatic three-mode entangled states generated by the combination of two-mode SPDCs interactions.
  arXiv  Detail & Related papers  (2020-01-20T10:39:28Z)

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.