scientific article; zbMATH DE number 1303338

MaRDI QIDQ4249891zbMATH OpenFDO

Authors Christoph Benzmüller, Michael Kohlhase

Publication date 12 January 2000

zbMATH Keywords

automated theorem-provinghigher-order unificationhigher-order resolutionHenkin model semantics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Comparing approaches to resolution based higher-order theorem proving
• scientific article; zbMATH DE number 1341621
• Higher order E-unification
• Higher-order semantics and extensionality

Cited in

(10)

• Set-of-support strategy for higher-order logic
• Higher-Order Multi-Valued Resolution
• scientific article; zbMATH DE number 5595970 (Why is no real title available?)
• HoCHC: a refutationally complete and semantically invariant system of higher-order logic modulo theories
• scientific article; zbMATH DE number 1341621 (Why is no real title available?)
• Higher-order semantics and extensionality
• Superposition with lambdas
• SAT-Inspired Higher-Order Eliminations
• Comparing approaches to resolution based higher-order theorem proving
• Superposition with lambdas

Describes a project that uses

Uses Software

• Leo

This page was built for publication:

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