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

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

Authors 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)

Recommendations

• Automated natural deduction prover and experiments
• scientific article; zbMATH DE number 4043301
• scientific article; zbMATH DE number 2176109
• 7th international conference on automated deduction, Napa, California, USA, May 14-16, 1984. Proceedings
• A resolution rule for well-formed formulae

Cited in

(6)

• Bucket elimination: A unifying framework for reasoning
• Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis
• Formal synthesis of a unification algorithm by the deductive-tableau method
• The Qu-Prolog unification algorithm: formalisation and correctness
• Using the prover ANDP to simplify orthogonality.
• Simplifying von Plato's axiomatization of constructive apartness geometry

Describes a project that uses

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)