Metraipolis › archive › dc_7fcff5505e83

Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions — arXiv:2611.00269

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.00269
License (as archived): CC0-1.0
Archived: 2026-11-03T10:51:32.764Z
SHA-256 of the archived text: 1be75761aea0d4ca4242adf9058975810dbf455c3125c3572bb287cfdc38f739
Stable URL of this page: https://metraipolis.com/documento/dc_7fcff5505e83

How to cite

Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions — arXiv:2611.00269 — arXiv (en), https://arxiv.org/abs/2611.00269 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_7fcff5505e83 (Metraipolis archive dc_7fcff5505e83, sha256 1be75761aea0d4ca4242adf9058975810dbf455c3125c3572bb287cfdc38f739)

BibTeX

@misc{dc7fcff5505e83,
  title = {Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions — arXiv:2611.00269},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.00269},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_7fcff5505e83; sha256 1be75761aea0d4ca4242adf9058975810dbf455c3125c3572bb287cfdc38f739},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.00269. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Automated theorem generation (ATG) seeks to construct new theorems rather than merely prove given conjectures. Existing approaches typically generate candidate statements that require subsequent proof or formal verification. We propose a constructive framework for ATG in first-order logic based on triangular standard contradictions. The method constructs minimally unsatisfiable clause sets from selected first-order literals, then forms theorems by retaining some clauses as premises and taking the negation of one clause, or a conjunction of clauses, as the conclusion. Minimal unsatisfiability ensures that the remaining premises are satisfiable, avoiding trivial inference by explosion, while unsatisfiability of the full set guarantees the resulting entailment. Theorems are therefore correct by construction, without a separate proof procedure for each instance. Extending the previously developed $\Delta_1$ generator, we introduce seven methods, $\Delta_2$--$\Delta_8$, forming a unified family of eight theorem-generation methods. Four generators, $\Delta_1$--$\Delta_4$, have been implemented and released. We also formulate a general $\Delta$-class method encompassing the family. Combinatorial analysis demonstrates the capacity to generate large numbers of distinct theorems systematically. This framework offers a principled foundation for automated theorem discovery and the construction of logically guaranteed knowledge.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2611.00269 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-03T10:49:38.234Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).