Comparing approaches to resolution based higher-order theorem proving

DOI10.1023/A:1020840027781zbMath1020.03011OpenAlexW2021219068MaRDI QIDQ1868166

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

higher-order logicfull extensionalityHenkin completenesshigher-order resolutionresolution-based higher-order theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (4)

The higher-order prover \textsc{Leo}-II ⋮ Combined reasoning by automated cooperation ⋮ CERES in higher-order logic ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic

Uses Software

• TPS
• Leo

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