Unification under a mixed prefix
DOI10.1016/0747-7171(92)90011-RzbMATH Open0768.68067OpenAlexW2050702141MaRDI QIDQ1201348FDOQ1201348
Authors: 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
Recommendations
unificationunifiersraisingSkolemizationconjunctions of equations between simply typed \(\lambda\)-termsmixed prefixquantifier alternation
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Completeness in the theory of types
- Resolution in type theory
- Title not available (Why is that?)
- Intuitionistic propositional logic is polynomial-space complete
- General models and extensionality
- Proving and applying program transformations expressed with second-order patterns
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Natural deduction as higher-order resolution
- The undecidability of the second-order unification problem
- The foundation of a generic theorem prover
- Higher-order unification revisited: Complete sets of transformations
- Higher-order unification with dependent function types
- Title not available (Why is that?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
- Title not available (Why is that?)
- The undecidability of unification in third order logic
- A Complete Mechanization of Second-Order Type Theory
- Mechanizing \(\omega\)-order type theory through unification
- Higher-order Horn clauses
Cited In (34)
- Third-order matching in the polymorphic lambda calculus
- Higher-Order Multi-Valued Resolution
- On extensibility of proof checkers
- Mechanized metatheory revisited
- Functions-as-constructors higher-order unification: extended pattern unification
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Unification with extended patterns
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Hybrid linear logic, revisited
- Nominal abstraction
- Hilbert's epsilon as an operator of indefinite committed choice
- Recasting ML\(^{\text F}\)
- Verifying termination and reduction properties about higher-order logic programs
- Higher order unification via explicit substitutions
- Types for modules
- Set theory for verification. I: From foundations to functions
- On the role of names in reasoning about \(\lambda\)-tree syntax specifications
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- COCHIS: stable and coherent implicits
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Third order matching is decidable
- A proof procedure for the logic of hereditary Harrop formulas
- A two-level logic approach to reasoning about computations
- Implementing type theory in higher order constraint logic programming
- Implementing tactics and tacticals in a higher-order logic programming language
- Translating higher-order clauses to first-order clauses
- The undecidability of proof search when equality is a logical connective
- Proof-term synthesis on dependent-type systems via explicit substitutions
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Tactics and parameters
- Higher order disunification: some decidable cases
- A colored version of the \(\lambda\)-calculus
- Reasoning in Abella about structural operational semantics specifications
Uses Software
This page was built for publication: Unification under a mixed prefix
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1201348)
