scientific article; zbMATH DE number 3878393

zbMATH Open0551.68075MaRDI QIDQ3343471FDOQ3343471

Authors: Peter B. Andrews, Eve Longini Cohen, Dale Miller, Frank Pfenning 

Publication date: 1984

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

Recommendations

• TPS: A theorem-proving system for classical type theory
• scientific article
• TPS: A hybrid automatic-interactive system for developing proofs
• scientific article
• On sets, types, fixed points, and checkerboards

zbMATH Keywords

higher order logic

Mathematics Subject Classification ID

Cited In (22)

• Higher-order unification, polymorphism, and subsorts
• Improving automation for higher-order proof steps
• Higher order E-unification
• The foundation of a generic theorem prover
• Extensional higher-order paramodulation in Leo-III
• Higher-order unification revisited: Complete sets of transformations
• One method of constructing a formal system
• Set-of-support strategy for higher-order logic
• On connections and higher-order logic
• Unification theory
• What holds in a context?
• Set theory for verification. I: From foundations to functions
• Title not available (Why is that?)
• Automating Coherent Logic
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• A compact representation of proofs
• Unification under a mixed prefix
• Title not available (Why is that?)
• Higher-order unification with dependent function types
• Simple second-order languages for which unification is undecidable
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• A unification algorithm for second-order monadic terms

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