Extraction of Expansion Trees

Area of Science:

• Automated reasoning
• Mathematical logic
• Computer science

Background:

• Proof mining aims to extract computationally useful information from mathematical proofs.
• The original CERES method extracts expansion trees from normalized proofs (ACNF) after cut-elimination.
• This process can be computationally intensive and requires proof normalization.

Purpose of the Study:

• To develop a novel method for extracting expansion trees from first-order logic proofs with equality.
• To avoid the computationally expensive proof normalization step required by the standard CERES method.
• To demonstrate the efficiency and performance benefits of the new method.

Main Methods:

• A new proof mining technique based on cut-elimination by resolution (CERES) is defined.
• Expansion trees are extracted directly from resolution refutations and their proof projections, bypassing normalization.
• The asymptotic performance of the new method is theoretically analyzed and compared to the standard approach.

Main Results:

• The novel CERES method successfully extracts expansion trees without requiring proof normalization.
• The new method demonstrates superior asymptotic performance compared to the standard CERES method.
• Experimental comparisons confirm the practical efficiency gains of the new method over the existing one.

Conclusions:

• The developed proof mining method offers a more efficient alternative for extracting expansion trees in first-order logic with equality.
• Avoiding proof normalization significantly improves both theoretical performance and practical efficiency.
• This advancement has implications for automated reasoning and the extraction of computational content from proofs.