scientific article; zbMATH DE number 1303338

zbMATH Open0928.03004MaRDI QIDQ4249891FDOQ4249891

Authors: Christoph Benzmüller, Michael Kohlhase 

Publication date: 12 January 2000

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (10)

• SAT-Inspired Higher-Order Eliminations
• Superposition with lambdas
• Higher-Order Multi-Valued Resolution
• Title not available (Why is that?)
• Higher-order semantics and extensionality
• Superposition with lambdas
• Set-of-support strategy for higher-order logic
• Comparing approaches to resolution based higher-order theorem proving
• HoCHC: a refutationally complete and semantically invariant system of higher-order logic modulo theories
• Title not available (Why is that?)

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)