登入選單

返回Google圖書搜尋

Investigations Into Proof-search in a System of First-order Dependent Function Types

University of Edinburgh. Department of Computer Science. Laboratory for Foundations of Computer ScienceDavid PymLincoln Wallen

出版	University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1990
URL	http://books.google.com.hk/books?id=5CRSGwAACAAJ&hl=&source=gbs_api

註釋

Our methods exploit certain forms of subformula property and reduction ordering -- a notion introduced by Bibel for classical logic, and extended by Wallen to various non-classical logics -- to obtain a search calculus for which we are able to define notions of compatibility and intrinsic well-typing between a derivation [psi] and a substitution [sigma] calculated by unification which closes [psi] (a derivation is closed when all of its leaves are axioms). Compatibility is an acyclicity test, a generalization of the occurs-check which, subject to intrinsic well-typing, determines whether the derivation [psi] and substitution [sigma] together constitute a proof.