Natural deduction as higher-order resolution
- 31 October 1986
- journal article
- Published by Elsevier in The Journal of Logic Programming
- Vol. 3 (3) , 237-258
- https://doi.org/10.1016/0743-1066(86)90015-4
Abstract
No abstract availableKeywords
All Related Versions
This publication has 19 references indexed in Scilit:
- A look at TPSPublished by Springer Nature ,2005
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- A Survey of the Project AutomathPublished by Elsevier ,1994
- Lessons learned from LCF: A Survey of Natural Deduction ProofsThe Computer Journal, 1985
- The use of machines to assist in rigorous proofPhilosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences, 1984
- Automating Higher-Order LogicContemporary Mathematics, 1984
- The undecidability of the second-order unification problemTheoretical Computer Science, 1981
- Mechanizing ω-order type theory through unificationTheoretical Computer Science, 1976
- A unification algorithm for typed
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972