Resolution in type theory

DOI10.2307/2269949zbMath0231.02038OpenAlexW4237061074MaRDI QIDQ5638281

Peter B. Andrews

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

Mathematics Subject Classification ID

Related Items (53)

Set-of-support strategy for higher-order logic ⋮ Upper bounds for standardizations and an application ⋮ Cut-elimination for quantified conditional logic ⋮ A semantics for \(\lambda \)Prolog ⋮ A compact representation of proofs ⋮ Andrews Skolemization may shorten resolution proofs non-elementarily ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY ⋮ TPS: A hybrid automatic-interactive system for developing 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 ⋮ TPS: A theorem-proving system for classical type theory ⋮ Schematic refutations of formula schemata ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Effective Skolemization ⋮ lambda-normal forms in an intensional logic for English ⋮ On connections and higher-order logic ⋮ Analytic tableaux for higher-order logic with choice ⋮ General models, descriptions, and choice in type theory ⋮ Automatic theorem proving. II ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ Theorem proving modulo ⋮ Combined reasoning by automated cooperation ⋮ Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ Unification under a mixed prefix ⋮ A simple proof that super-consistency implies cut elimination ⋮ Resolution is cut-free ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ System Description: The Proof Transformation System CERES ⋮ A unification algorithm for typed \(\bar\lambda\)-calculus ⋮ A sequent calculus for type assignment ⋮ A unification algorithm for typed \(\overline\lambda\)-calculus ⋮ CERES in higher-order logic ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Abstract deduction and inferential models for type theory ⋮ Mechanizing \(\omega\)-order type theory through unification ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ System Description: GAPT 2.0 ⋮ Extending SMT solvers to higher-order logic ⋮ Typing and computational properties of lambda expressions ⋮ On the logic of unification ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Mechanized metatheory revisited ⋮ The linked conjunct method for automatic deduction and related search techniques ⋮ The completeness theorem for typing lambda-terms ⋮ Higher order unification via explicit substitutions ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory ⋮ Annual Meeting of the Association for Symbolic Logic ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Cites Work

• A transfinite type theory with type variables
• A proof of cut-elimination theorem in simple type-theory
• A Machine-Oriented Logic Based on the Resolution Principle
• An Abstract form of the church-rosser theorem. I
• A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
• Unnamed Item

This page was built for publication: Resolution in type theory