scientific article
From MaRDI portal
Publication:2751368
zbMath1011.03005MaRDI QIDQ2751368
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
surveydecidabilityhigher-order unificationunification algorithmscontext unificationpattern-matchingsemi-decision algorithmformalizations of set theory
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Set theory (03E99)
Related Items
Higher-order pattern anti-unification in linear time, Higher-Ranked Annotation Polymorphic Dependency Analysis, Nominal unification, Probabilistic modelling, inference and learning using logical theories, Simplifying the signature in second-order unification, Unification for $$\lambda $$ -calculi Without Propagation Rules, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, Unnamed Item, Unnamed Item, Higher-order pattern generalization modulo equational theories, Decidability of bounded higher-order unification, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, A Clausal Approach to Proof Analysis in Second-Order Logic, Superposition with lambdas, Nominal Unification from a Higher-Order Perspective, Superposition with lambdas, Extending SMT solvers to higher-order logic, Automorphisms of types and their applications
