Handbook of Automated Reasoning

Chapter 8

Unification Theory

Franz Baader; Wayne Snyder

Paliath Narendran; Manfred Schmidt-Schauss; Klaus Schulz Second readers

Contents

1  Introduction    447

1.1  What is unification?    447

1.2  History and applications    448

1.3  Approach    450

2  Syntactic unification    450

2.1  Definitions    451

2.2  Unification of terms    452

2.3  Unification of term dags    459

3  Equational unification    469

3.1  Basic notions    469

3.2  New issues    473

3.3  Reformulations    475

3.4  Survey of results for specific theories    482

4  Syntactic methods for E-unification    488

4.1  E-unification in arbitrary theories    488

4.2  Restrictions on E-unification in arbitrary theories    495

4.3  Narrowing    495

4.4 ...