Unification under a mixed prefix

DOI10.1016/0747-7171(92)90011-RzbMath0768.68067OpenAlexW2050702141MaRDI QIDQ1201348

S. Singh

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

zbMATH Keywords

unificationunifiersraisingSkolemizationconjunctions of equations between simply typed \(\lambda\)-termsmixed prefixquantifier alternation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)

Related Items (34)

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

• Elf

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

This page was built for publication: Unification under a mixed prefix