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)
- Authors: Christoph Wernhard
- 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
- 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 [2.7412662946127755]
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) - Decoding Structure-Spectrum Relationships with Physically Organized
Latent Spaces [6.36075035468233]
A new semi-supervised machine learning method for the discovery of structure-spectrum relationships is developed and demonstrated.
This method constructs a one-to-one mapping between individual structure descriptors and spectral trends.
The RankAAE methodology produces a continuous and interpretable latent space, where each dimension can track an individual structure descriptor.
arXiv Detail & Related papers (2023-01-11T21:30:22Z) - 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.