scientific article; zbMATH DE number 3878393

MaRDI QIDQ3343471zbMATHFDO

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

Publication date 1984

zbMATH Keywords

higher order logic

Mathematics Subject Classification ID

Recommendations

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

Cited in

(22)

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

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)