Comparing approaches to resolution based higher-order theorem proving

DOI10.1023/A:1020840027781MaRDI QIDQ1868166zbMATH OpenOpenAlexFDO

Authors Christoph Benzmüller

Publication date 27 April 2003

Published in Synthese (Search for Journal in Brave)

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

zbMATH Keywords

full extensionalityHenkin completenesshigher-order logichigher-order resolutionresolution-based higher-order theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

Four approaches to resolution-based higher-order theorem proving are investigated: Andrews' higher-order resolution approach; Huet's constrained resolution approach; higher-order E-resolution; and extensional higher-order resolution. The author focuses on Henkin completeness and full extensionality. The paper demonstrates that simply adding extensionality axioms to the search space increases the amount of blind search. Higher-order E-unification and R-resolution improves the situation but it does still not provide a general solution. Extensional higher-order resolution is the sole studied approach that can completely avoid the extensionality axioms.

Recommendations

• scientific article; zbMATH DE number 1303338
• Higher order E-unification
• scientific article; zbMATH DE number 1341621
• scientific article; zbMATH DE number 1552534
• The Clausal Theory of Types

Cited in

(12)

• The higher-order prover \textsc{Leo}-II
• Resolution-Like Theorem Proving for High-Level Conditions
• A Clausal Approach to Proof Analysis in Second-Order Logic
• scientific article; zbMATH DE number 1303338 (Why is no real title available?)
• scientific article; zbMATH DE number 1134678 (Why is no real title available?)
• GoedelGod
• Set-of-support strategy for higher-order logic
• CERES in higher-order logic
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
• Automation of Boolos' Curious Inference in Isabelle/HOL
• Combined reasoning by automated cooperation

Describes a project that uses

Uses Software

• TPS
• Leo

This page was built for publication: Comparing approaches to resolution based higher-order theorem proving

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