CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)

• URL: http://arxiv.org/abs/2207.08453v1
• Date: Mon, 18 Jul 2022 09:15:08 GMT
• Title: CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)
• Abstract summary: CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP. From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications. For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP, which puts a recent formal view centered around proof structures into practice. From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications, making it attractive as a basis for developing and evaluating novel techniques. CD Tools includes specialized provers based on the enumeration of proof structures. We focus here on one of these, SGCD, which permits to blend goal- and axiom-driven proof search in particularly flexible ways. In purely goal-driven configurations it acts similarly to a prover of the clausal tableaux or connection method family. In blended configurations its performance is much stronger, close to state-of-the-art provers, while emitting relatively short proofs. Experiments show characteristics and application possibilities of the structure generating approach realized by that prover. For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.

Related papers

• Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB [0.2676349883103403]
  Event-B is a formal method rooted in predicate logic and set theory.<n>We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction.<n>By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation.
  arXiv  Detail & Related papers  (2026-07-23T11:16:32Z)
• All Circuits Lead to Rome: Rethinking Functional Anisotropy in Circuit and Sheaf Discovery for LLMs [61.02007370456733]
  We show that a single task can be supported by multiple, structurally distinct circuits or sheaves that are simultaneously faithful, sparse, and complete.<n>We propose a Distributive Circuit Hypothesis and provide a theoretical analysis demonstrating that non-unique, low-overlap circuit explanations arise naturally from high-dimensional superposition.
  arXiv  Detail & Related papers  (2026-05-12T19:21:23Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• Compact Prompting in Instruction-tuned LLMs for Joint Argumentative Component Detection [9.542561151544984]
  Argumentative component detection (ACD) is a core subtask of Argument(ation) Mining (AM)<n>We propose a novel approach based on instruction-tuned Large Language Models (LLMs) using compact instruction-based prompts.<n> Experiments on standard benchmarks show that our approach achieves higher performance compared to state-of-the-art systems.
  arXiv  Detail & Related papers  (2026-03-03T15:32:58Z)
• When Agda met Vampire [3.373200015661363]
  We aim to integrate proof assistants with automated theorem provers (ATPs) in a simple way.<n>Most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory.<n>We produce a prototype system for Agda proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check.
  arXiv  Detail & Related papers  (2026-02-21T14:19:56Z)
• Disco-RAG: Discourse-Aware Retrieval-Augmented Generation [81.53888908988756]
  We propose Disco-RAG, a discourse-aware framework that injects discourse signals into the generation process.<n>Our method constructs intra-chunk discourse trees to capture local hierarchies and builds inter-chunk rhetorical graphs to model cross-passage coherence.<n>Experiments on question answering and long-document summarization benchmarks show the efficacy of our approach.
  arXiv  Detail & Related papers  (2026-01-07T20:32:50Z)
• Gödel's Poetry [0.0]
  We introduce a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation.<n>We achieve a 90.4% pass rate on miniF2F without decomposition.<n>A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities.
  arXiv  Detail & Related papers  (2025-12-16T10:00:01Z)
• Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
  Generative Logic (GL) is a deterministic architecture that starts from usersupplied axiomatic definitions.<n>GL enumerates conjectures, applies normalization, type, and CE filter, and automatically reconstructs machine-checkable proofs.
  arXiv  Detail & Related papers  (2025-07-25T17:29:19Z)
• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup.
  arXiv  Detail & Related papers  (2024-09-23T13:38:31Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
  We propose a novel proof aggregation approach based on OR logic for Merkle tree inclusion proofs. We achieve a proof size independent of the number of leaves in the tree, and verification can be performed using any single valid leaf hash. The proposed techniques have the potential to significantly enhance the scalability, efficiency, and flexibility of zero-knowledge proof systems.
  arXiv  Detail & Related papers  (2024-05-13T17:15:38Z)
• Navigating the Structured What-If Spaces: Counterfactual Generation via Structured Diffusion [20.20945739504847]
  We introduce Structured Counterfactual diffuser or SCD, the first plug-and-play framework leveraging diffusion for generating counterfactual explanations in structured data. Our experiments show that our counterfactuals not only exhibit high plausibility compared to the existing state-of-the-art but also show significantly better proximity and diversity.
  arXiv  Detail & Related papers  (2023-12-21T07:05:21Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)
• Large-scale Pre-trained Models are Surprisingly Strong in Incremental Novel Class Discovery [76.63807209414789]
  We challenge the status quo in class-iNCD and propose a learning paradigm where class discovery occurs continuously and truly unsupervisedly. We propose simple baselines, composed of a frozen PTM backbone and a learnable linear classifier, that are not only simple to implement but also resilient under longer learning scenarios.
  arXiv  Detail & Related papers  (2023-03-28T13:47:16Z)
• Investigations into Proof Structures [0.8287206589886879]
  We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Lukasiewicz.
  arXiv  Detail & Related papers  (2023-02-14T12:29:39Z)
• Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving [0.0]
  We introduce here this "combinator term as proof structure" approach to automated first-order proving. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method.
  arXiv  Detail & Related papers  (2022-09-26T11:23:17Z)
• GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
  We propose GERE, the first system that retrieves evidences in a generative fashion. The experimental results on the FEVER dataset show that GERE achieves significant improvements over the state-of-the-art baselines.
  arXiv  Detail & Related papers  (2022-04-12T03:49:35Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)

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.