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

DOI10.1023/A:1005749401809zbMATH Open0871.03004OpenAlexW1499666987MaRDI QIDQ679252FDOQ679252

Da-Fa 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

automated theorem provingGentzen systemhalting problemAndrews 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)

Cited In (6)

• Bucket elimination: A unifying framework for reasoning
• Formal synthesis of a unification algorithm by the deductive-tableau method
• Using the prover ANDP to simplify orthogonality.
• The Qu-Prolog unification algorithm: formalisation and correctness
• 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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q679252)