scientific article; zbMATH DE number 3878393

MaRDI QIDQ3343471zbMATH OpenFDO

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

(24)

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

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)