Resolution in type theory
From MaRDI portal
Publication:5638281
DOI10.2307/2269949zbMath0231.02038MaRDI QIDQ5638281
Publication date: 1971
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2269949
03B40: Combinatory logic and lambda calculus
Related Items
General models, descriptions, and choice in type theory, TPS: A hybrid automatic-interactive system for developing proofs, On connections and higher-order logic, Combined reasoning by automated cooperation, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, A compact representation of proofs, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Unification theory, lambda-normal forms in an intensional logic for English, Unification under a mixed prefix, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, Mechanizing \(\omega\)-order type theory through unification, A semantics for \(\lambda \)Prolog, Theorem proving modulo, Typing and computational properties of lambda expressions, On the logic of unification, Higher-order unification revisited: Complete sets of transformations, The linked conjunct method for automatic deduction and related search techniques, The completeness theorem for typing lambda-terms, Higher order unification via explicit substitutions, TPS: A theorem-proving system for classical type theory, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, A Clausal Approach to Proof Analysis in Second-Order Logic, Annual Meeting of the Association for Symbolic Logic, Automatic theorem proving. II, A sequent calculus for type assignment, Upper bounds for standardizations and an application
Cites Work
