5 papers
Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning
Yang Xu, Jun Liu, Shuwei Chen +2
Neuro-symbolic reasoning increasingly demands frameworks that unite the formal rigor of logic with the interpretability of large language models (LLMs). We introduce an end to end…
An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
Yang Xu, Peiyao Liu, Shuwei Chen +1
Currently, there is a lack of rigorous theoretical system for systematically generating non-trivial and logically valid theorems. Addressing this critical gap, this paper conducts…
Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
Yang Xu, Shuwei Chen, Jun Liu +2
Automated deduction lies at the core of Artificial Intelligence (AI), underpinning theorem proving, formal verification, and logical reasoning. Despite decades of progress, reconci…
Dynamic Automated Deduction by Contradiction Separation: The Standard Extension Algorithm
Yang Xu, Xingxing He, Shuwei Chen +2
Automated deduction seeks to enable machines to reason with mathematical precision and logical completeness. Classical resolution-based systems, such as Prover9, E, and Vampire, re…
Contradictions
Yang Xu, Shuwei Chen, Xiaomei Zhong +2
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 classica…