Flat matching

Abstract. Flat theory with sequence variables and flexible arity symbols has infinitary matching and unification type. Decidability of general unification is shown and a unification procedure to enumerate minimal complete set of unifiers is described. The flat matching procedure is compared with the flat matching algorithm implemented in the Mathematica system.

• Type: Journal
• Year: 2008
• Where: JSC
• Authors: Temur Kutsia
• Keywords: Flat Matching Procedure, Flexible Arity Symbols, JSC 2008, Unification Procedure