Publication:4364370
From MaRDI portal
zbMath0888.03007MaRDI QIDQ4364370
Christophe Ringeissen, Claude Kirchner
Publication date: 17 November 1997
rewrite system; lambda-calculus; explicit substitution; first-order unification; higher-order \(E\)-unification; rule-based unification procedure
Related Items
Proof-term synthesis on dependent-type systems via explicit substitutions, Theorem proving modulo, Higher order unification via explicit substitutions