Building Theorems from Carefully Designed Contradictions

From finding proofs to constructing statements

Automated theorem proving usually starts with a target: a statement whose truth must be established from given assumptions. Automated theorem generation asks a different question—what statements should the machine produce in the first place?

In a preprint submitted on October 30, Yang Xu, Shuwei Chen, Hailin Guo and Jun Liu describe a way to generate theorems in first-order logic by constructing carefully organised contradictions. Rather than proposing a candidate and asking a separate prover to establish it, their approach builds logical validity into the generation process.

The distinction matters, but it is not a claim that machines can now discover useful mathematics automatically. The paper focuses on generating valid relationships between premises and conclusions. Whether those relationships are interesting or practically valuable remains a separate question.

A contradiction with nothing to spare

The central ingredient is a minimally unsatisfiable clause set. A clause is a collection of literals joined by “or”; a literal is an atomic statement or its negation. A clause set requires all its clauses to hold together.

An unsatisfiable set has no interpretation in which every clause is true. It is minimally unsatisfiable when removing any single clause makes the remaining collection satisfiable. Every clause is therefore essential to the contradiction.

That property gives the authors their theorem-generation mechanism. Select a clause, remove it, and retain the others as premises. Those premises logically imply the negation of the removed clause: otherwise, all the original clauses could hold together, contradicting the starting construction.

The method also allows several clauses to be removed. In that case, the conclusion negates their conjunction—it says they cannot all hold together—not that every removed clause must individually be false.

Why consistent premises matter

Unsatisfiability alone would not provide the guarantee the researchers want. In classical logic, inconsistent premises entail any conclusion, a rule known as the principle of explosion. Such an inference would say little about the particular conclusion generated.

Minimal unsatisfiability prevents that problem here. Removing a clause leaves satisfiable premises; removing further clauses cannot destroy that satisfiability. The resulting entailment therefore does not depend on starting with inconsistent assumptions.

The logical principle is established at the level of the construction. Once its conditions are met, the authors argue, each generated instance does not need a separate proof search. This is different from dispensing with mathematical justification: the paper supplies arguments intended to establish why the generation procedures work.

What makes the construction triangular

The researchers organise literals and their negations in structures they call triangular standard contradictions. “Standard contradiction” is terminology developed in their earlier work, rather than a conventional name in mathematical logic. The diagrams specify how literals are assembled into clauses; their connecting lines are not additional logical operations.

The paper extends the earlier Delta-1 method with seven methods, Delta-2 through Delta-8. It also presents a general Delta-class construction. The authors report that implementations of Delta-1 through Delta-4 have been released.

These constructions have explicit restrictions: the generating literals use pairwise distinct predicate symbols, and none uses the equality predicate. Those conditions support the satisfiability arguments. Under the stated conditions, the general construction produces a minimally unsatisfiable structure with a minimum of 2n literal occurrences for n generating literals.

Many outputs, but usefulness is another test

The paper analyses how the number of outputs grows as literals are reordered, structures are extended and clauses are assigned to premises or conclusions. A minimally unsatisfiable set containing n + 1 clauses yields 2^(n+1) − 2 nonempty, proper choices of clauses to move into the conclusion.

The authors count theorems as different when their premise sets or conclusions differ. That is a formal distinction between outputs, not a demonstration that each represents a separate mathematical insight.

The proposed applications include structured knowledge for automated reasoning, theorem-proving benchmarks and possible combinations with neuro-symbolic or language-model systems. These are prospects rather than demonstrated benefits. The authors explicitly leave meaningful interpretation, practical application and assessment of interestingness for future work. Their contribution is a proposed route from designed contradictions to valid entailments—not yet a method for deciding which generated theorems deserve attention.