Unification under a mixed prefix
From MaRDI portal
Publication:1201348
DOI10.1016/0747-7171(92)90011-RzbMath0768.68067OpenAlexW2050702141MaRDI QIDQ1201348
Publication date: 17 January 1993
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0747-7171(92)90011-r
unificationunifiersraisingSkolemizationconjunctions of equations between simply typed \(\lambda\)-termsmixed prefixquantifier alternation
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)
Related Items
Third order matching is decidable, Functions-as-constructors higher-order unification: extended pattern unification, The undecidability of proof search when equality is a logical connective, Types for modules, Verifying termination and reduction properties about higher-order logic programs, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, A two-level logic approach to reasoning about computations, Choices in representation and reduction strategies for lambda terms in intensional contexts, Higher order disunification: Some decidable cases, Nominal abstraction, On extensibility of proof checkers, A Survey of the Proof-Theoretic Foundations of Logic Programming, Idris, a general-purpose dependently typed programming language: Design and implementation, Hilbert's epsilon as an operator of indefinite committed choice, Third-order matching in the polymorphic lambda calculus, Translating higher-order clauses to first-order clauses, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Tactics and Parameters, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Proof-term synthesis on dependent-type systems via explicit substitutions, Reasoning in Abella about Structural Operational Semantics Specifications, On the Role of Names in Reasoning about λ-tree Syntax Specifications, Higher-Order Multi-Valued Resolution, COCHIS: Stable and coherent implicits, Recasting ML\(^{\text F}\), Unification with extended patterns, A colored version of the λ-calculus, Implementing type theory in higher order constraint logic programming, Hybrid linear logic, revisited, Mechanized metatheory revisited, Higher order unification via explicit substitutions, Implementing tactics and tacticals in a higher-order logic programming language, A proof procedure for the logic of hereditary Harrop formulas, Set theory for verification. I: From foundations to functions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The undecidability of the second-order unification problem
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- Proving and applying program transformations expressed with second-order patterns
- Intuitionistic propositional logic is polynomial-space complete
- The foundation of a generic theorem prover
- Higher-order unification revisited: Complete sets of transformations
- Higher-order Horn clauses
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Natural deduction as higher-order resolution
- Higher-order unification with dependent function types
- Resolution in type theory
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- General models and extensionality
- Completeness in the theory of types
