Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving

DOI10.1023/A:1005749401809zbMath0871.03004OpenAlexW1499666987MaRDI QIDQ679252

Dafa Li

Publication date: 9 September 1997

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005749401809

zbMATH Keywords

halting problemautomated theorem provingGentzen systemAndrews challenge problemautomatic natural deduction proving systemunification algorithm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (3)

Using the prover ANDP to simplify orthogonality. ⋮ Simplifying von Plato's axiomatization of constructive apartness geometry ⋮ Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis

Uses Software

• ETPS
• MUSCADET

This page was built for publication: Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving