scientific article

zbMath1011.03005MaRDI QIDQ2751368

Gilles Dowek

Publication date: 27 August 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

surveydecidabilityhigher-order unificationunification algorithmscontext unificationpattern-matchingsemi-decision algorithmformalizations of set theory

Mathematics Subject Classification ID

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 (18)

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

This page was built for publication: