Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction

• URL: http://arxiv.org/abs/2510.10701v1
• Date: Sun, 12 Oct 2025 17:03:33 GMT
• Title: Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
• Authors: Yang Xu, Shuwei Chen, Jun Liu, Feng Cao, Xingxing He,
• Abstract summary: 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.
• Score: 11.18154335347018
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated deduction lies at the core of Artificial Intelligence (AI), underpinning theorem proving, formal verification, and logical reasoning. Despite decades of progress, reconciling deductive completeness with computational efficiency remains an enduring challenge. Traditional reasoning calculi, grounded in binary resolution, restrict inference to pairwise clause interactions and thereby limit deductive synergy among multiple clauses. The Contradiction Separation Extension (CSE) framework, introduced in 2018, proposed a dynamic multi-clause reasoning theory that redefined logical inference as a process of contradiction separation rather than sequential resolution. While that work established the theoretical foundation, its algorithmic realization remained unformalized and unpublished. This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation. The ETM unifies multiple contradiction-building strategies, including the earlier Standard Extension method, within a triangular geometric framework that supports flexible clause interaction and dynamic synergy. ETM serves as the algorithmic core of several high-performance theorem provers, CSE, CSE-E, CSI-E, and CSI-Enig, whose competitive results in standard first-order benchmarks (TPTP problem sets and CASC 2018-2015) empirically validate the effectiveness and generality of the proposed approach. By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning, offering new directions for future research in logical inference and theorem proving.

Related papers

• Multi-Path Collaborative Reasoning via Reinforcement Learning [54.8518809800168]
  Chain-of-Thought (CoT) reasoning has significantly advanced the problem-solving capabilities of Large Language Models (LLMs)<n>Recent methods attempt to address this by generating soft abstract tokens to enable reasoning in a continuous semantic space.<n>We propose Multi-Path Perception Policy Optimization (M3PO), a novel reinforcement learning framework that explicitly injects collective insights into the reasoning process.
  arXiv  Detail & Related papers  (2025-12-01T10:05:46Z)
• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  Diffusion language models (dLLMs) offer a promising, non-autoregressive paradigm for text generation.<n>Current reinforcement learning approaches often rely on sparse, outcome-based rewards.<n>We argue that this stems from a fundamental mismatch with the natural structure of reasoning.
  arXiv  Detail & Related papers  (2025-10-02T00:34:15Z)
• Contradictions [9.602468627573215]
  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.
  arXiv  Detail & Related papers  (2025-09-07T13:47:51Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  Chain-of-thought (CoT) reasoning enables large language models to break down complex problems into interpretable intermediate steps.<n>We introduce groundingS, a framework that formulates CoT reasoning as a Markov decision process (MDP) with latent state transitions.<n>We show improvements in reasoning accuracy, diversity, and exploration efficiency across benchmark reasoning tasks.
  arXiv  Detail & Related papers  (2025-07-10T21:32:18Z)
• Adaptive Termination for Multi-round Parallel Reasoning: An Universal Semantic Entropy-Guided Framework [12.361554676966552]
  Recent advances in large language models (LLMs) have accelerated progress toward artificial general intelligence.<n>We aim to design a flexible test-time collaborative inference framework that exploits the complementary strengths of both sequential and parallel reasoning paradigms.
  arXiv  Detail & Related papers  (2025-07-09T13:28:35Z)
• PixelThink: Towards Efficient Chain-of-Pixel Reasoning [70.32510083790069]
  PixelThink is a simple yet effective scheme that integrates externally estimated task difficulty and internally measured model uncertainty.<n>It learns to compress reasoning length in accordance with scene complexity and predictive confidence.<n> Experimental results demonstrate that the proposed approach improves both reasoning efficiency and overall segmentation performance.
  arXiv  Detail & Related papers  (2025-05-29T17:55:49Z)
• The Curse of CoT: On the Limitations of Chain-of-Thought in In-Context Learning [56.574829311863446]
  Chain-of-Thought (CoT) prompting has been widely recognized for its ability to enhance reasoning capabilities in large language models (LLMs)<n>We demonstrate that CoT and its reasoning variants consistently underperform direct answering across varying model scales and benchmark complexities.<n>Our analysis uncovers a fundamental hybrid mechanism of explicit-implicit reasoning driving CoT's performance in pattern-based ICL.
  arXiv  Detail & Related papers  (2025-04-07T13:51:06Z)
• On the Diagram of Thought [20.805936414171892]
  Large Language Models (LLMs) excel at many tasks but often falter on complex problems that require structured, multi-step reasoning.<n>We introduce the Diagram of Thought (DoT), a new framework that enables a single LLM to build and navigate a mental map of its reasoning.
  arXiv  Detail & Related papers  (2024-09-16T07:01:41Z)
• Answering Causal Queries at Layer 3 with DiscoSCMs-Embracing Heterogeneity [0.0]
  This paper advocates for the Distribution-consistency Structural Causal Models (DiscoSCM) framework as a pioneering approach to counterfactual inference.
  arXiv  Detail & Related papers  (2023-09-17T17:01:05Z)
• 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)
• Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
  It is common to address the curse of dimensionality in Markov decision processes (MDPs) by exploiting low-rank representations. We consider an alternative definition of linear MDPs that automatically ensures normalization while allowing efficient representation learning. We demonstrate superior performance over existing state-of-the-art model-based and model-free algorithms on several benchmarks.
  arXiv  Detail & Related papers  (2022-07-14T18:18:02Z)

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.