Resolution in type theory
From MaRDI portal
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A proof of cut-elimination theorem in simple type-theory
- A transfinite type theory with type variables
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- An Abstract form of the church-rosser theorem. I
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
Cited in
(58)- 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 - 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 -calculus
- Mechanizing \(\omega\)-order type theory through unification
- A semantics for 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
- Andrews Skolemization may shorten resolution proofs non-elementarily
- Extending SMT solvers to higher-order logic
- Mechanized metatheory revisited
- Cut-elimination for quantified conditional logic
- Schematic refutations of formula schemata
- Extensional higher-order paramodulation in Leo-III
- System description: GAPT 2.0
- On the convergence of reduction-based and model-based methods in proof theory
- Glivenko and Kuroda for simple type theory
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- 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
- Analytic tableaux for higher-order logic with choice
- Superposition for lambda-free higher-order logic
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- General models, descriptions, and choice in type theory
- Analytic tableaux for higher-order logic with choice
- System Description: The Proof Transformation System CERES
- Set-of-support strategy for higher-order logic
- Superposition with lambdas
- Superposition with lambdas
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Effective Skolemization
- The TPS theorem proving system
- Arithmetic is necessary
- Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Extracting Herbrand systems from refutation schemata
- A simple proof that super-consistency implies cut elimination
- Herbrand's theorem in inductive proofs
- CERES in higher-order logic
- TPS: A hybrid automatic-interactive system for developing proofs
- On connections and higher-order logic
- Combined reasoning by automated cooperation
- Resolution is cut-free
- Abstract deduction and inferential models for type theory
This page was built for publication: Resolution in type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5638281)
