In 1988 I was a guest of the **FORMEL Project** at INRIA, as a wandering ABD. The forte of FORMEL was the unification algorithm, and I spent some time copying papers from a filing cabinet which, after my time, grew to be 3 or 4 filing cabinets and became known as the Formel Library. I hear that, as the project disbanded, the cabinets were donated to another institution and then subsequently lost. I copied 56 papers from the library and put them into 5 themed binders. Recently I was possessed of a desire to clean out a storage space I have been renting, to save money by giving back the space. The storage space is filled with items I can’t part with and never consult, including those 5 binders.

The obvious thing to do would be to scan and upload all of the papers to something like ResearchGate. However, this thought was nixed by the Academia StackExchange community. But what if there was something rare, valuable and irreplaceable in my collection? Well, I inventoried what I had, and, alas, there is no such animal. Almost all of the papers of any merit are available either freely or for large sums of money on the Internet. What if everything academic *should* be free? A workaround occurred to me: Summarize the essentials of rare or paywalled papers. I got an OK on this idea from the community, but I don’t have the time or the desire to carry it out. I also can’t guess how the library evolved after I left.

The intellectual property of my sample is not lost, even if the ideas have, to some extent, lost their hold on the world: One of the chief products of Formel was the CAML language, which, alas, has been pushed out on the rankings by it’s closest rival, Haskell, which is, itself, at the bottom of the list.

My binders were organized into 5 topics:

- Unification on first-order terms
- Derivations of the unification algorithm
- Knuth-Bendix critical-pair completion algorithm
- Completion in equational systems and term rewriting systems
- Complexity and expressibility of unification and completion

Here is what they contain (or contained, if I end up recycling them):

### Unification on first-order terms

- Unification associative. 1988. Laboratoire Informatique Theorique et Programmation. Abdulrab, Habib. Pecuchet, Jean-Pierre. No PDF found online.
- Presentation et evaluation de la complexite en moyenne d’algorithmes de filtrage dans les moteurs d’inference. 1988. Revue d’intelligence artificielle. Albert, Luc. No PDF found online.
- An efficient unification algorithm. 1973. Math Dept, U. of Waterloo. Baxter, Lewis Denver. No PDF found online.
- Properties of substitutions and unification. 1985. Journal of Symbolic Logic. Eder, Elmar. http://www.sciencedirect.com/science/article/pii/S0747717185800274
- An efficient unification algorithm. 1982. ACM Transactions on Programming Languages and Systems. Martelli, Alberto. Montanari, Ugo. https://dl.acm.org/citation.cfm?id=357169
- Efficient unification with infinite terms in logic programming. 1984. International conference on Fifth Generation Computer Systems 1984. Martelli, Alberto. Rossi, Gianfranco. No PDF found online.
- Linear unification. 1978. Journal of Computer and System Sciences. Paterson, M.S. Wegman, M.N. http://www.sciencedirect.com/science/article/pii/0022000078900430
- A short survey on the state of the art in matching and unification problems. 1978. SEKI-Projekt. Raulefs, P. Siekmann, J., Szabo, P., Unvericht, E.. https://dl.acm.org/citation.cfm?id=1089208.1089210
- Transformational systems and the algebraic structure of atomic formulas. 1970. Machine Intelligence. Reynolds, J. http://www.cs.cmu.edu/afs/cs/user/jcr/ftp/transysalg.pdf
- A machine-oriented logic based on the resolution principle. 1965. Journal of the ACM. Robinson, J.A. https://web.stanford.edu/class/linguist289/robinson65.pdf
- Computational logic: The unification computation. 1970. Machine Intelligence. Robinson, J.A. https://aitopics.org/download/classics:E35191E8
- Notes on unification. 1982. Universitat Karlsruhe. Siekmann, J. Szabo, P. No PDF found online.
- Delaying unification algorithms for lambda calculi. 1988. Theoretical Computer Science. Staples, John. https://www.sciencedirect.com/science/article/pii/0304397588901351

### Derivations of the unification algorithm

- Synthesis of a unification algorithm in a logic programming calculus. 1984. J. Logic Programming. Eriksson, Lars-Henrik. http://www.sciencedirect.com/science/article/pii/0743106684900207
- Computing Unification Algorithms. 1986. IEEE LICS. Kirchner, Claude. No PDF found online.
- Deductive Synthesis of the Unification Algorithm. 1983. Computer Program Synthesis Methodologies. Manna, Z. Waldinger, R. https://link.springer.com/chapter/10.1007/978-94-009-7019-9_8
- Verifying the Unification Algorithm in LCF. 1985. Science of Computer Programming. Paulson, Lawrence C. https://arxiv.org/ftp/cs/papers/9301/9301101.pdf
- A categorical unification algorithm. 1986. Category Theory and Computer Programming. Rydeheard D.E. Burstall R.M. https://link.springer.com/chapter/10.1007/3-540-17162-2_139
- The unification of terms: A category-theoretic algorithm. 1985. U. of Manchester. Rydeheard D.E. Burstall R.M. No PDF found online
- Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms. 1987. Category Theory and Computer Science. Rydeheard D.E. Stell, J.G.. https://link.springer.com/chapter/10.1007/3-540-18508-9_23

### Knuth-Bendix critical-pair completion algorithm

- Critical-pair criteria for the Knuth-Bendix completion procedure. 1986. SYMSAC. Bachmair, Leo. Dershowitz, Nachum. No PDF found online.
- Orderings for Equational Proofs. 1986. LICS. Bachmair, Leo. Dershowitz, Nachum, Hsiang, Jieh. No PDF found online.
- Algebraic simplification. 1983. Computer Algebra. Buchberger, B. Loos, R. https://link.springer.com/chapter/10.1007/978-3-7091-7551-4_2
- History and basic features of the critical-pair/completion procedure. 1987. Journal of Symbolic Computation. Buchberger, B. http://www.sciencedirect.com/science/article/pii/S0747717187800202
- Existence, Uniqueness, and Construction of Rewrite Systems. 1988. SIAM J. Comp. Dershowitz, N. Marcus, Leo, Tarlecki, Andrzej. No PDF found online
- Confluent reductions. 1980. Journal of the ACM. Huet, Gerard. https://dl.acm.org/purchase.cfm?id=322230&CFID=842652407&CFTOKEN=64558699
- A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. 1981. JCSS. Huet, Gerard. https://pdfs.semanticscholar.org/7504/2affac9fbef414858a9d77b19aedb4c008f2.pdf
- Inductive reasoning with incomplete specifications. 1986. Proc of Logic in CS Conference. Kapur, D. Musser, D.R. No PDF found online
- Simple Word Problems in Universal Algebras. 1983. Automated Reasoning. Knuth, D.E. Bendix, P.B. https://pdfs.semanticscholar.org/9487/7bdf8313565b90758a5e664764139857b358.pdf
- Reducing the Complexity of the Knuth-Bendix Completion Algorithm: A “Unification” of Different Approaches. 1985. EUROCAL ’85. Winkler, Franz. https://www.risc.jku.at/publications/download/risc_3519/paper_51.pdf
- A Church-Rosser theorem for reduction systems. 1981. ACM SYMSAC submission. Winkler, Franz. No PDF found online
- A Criterion for Eliminating Unnecessary Reductions in the Knuth-Bendix Algorithm. 1983. J. Bolyai Math Society. Winkler, Franz. Buchberger, Bruno. No PDF found online

### Completion in equational systems and term rewriting systems

- Automatic proofs by induction in theories without constructors. 1989. Information and Computation. Jouannaud, Jean-Pierre. Kounalis, Emmanuel. https://www.sciencedirect.com/science/article/pii/089054018990062X
- A general completion algorithm for equational term rewriting systems and its proof of correctness. 1983. CRIN. Kirchner, H. No PDF found online.
- Reveur-3: the implementation of a general completion procedure parameterized by built-in theories and strategies. 1987. Science of Computer Programming. Kirchner, Helene. Kirchner, Claude. https://www.sciencedirect.com/science/article/pii/0167642387900049
- An Overview of Completion Algorithms. 1985. EUROCAL ’85. Llopis de Trias, Regina. No PDF found online.
- Canonical forms for residue classes of polynomial ideals and term rewriting systems. 1983. Submitted to JACM. Llopis de Trias, Regina. No PDF found online.
- Complete Sets of Reductions for Some Equational Theories. 1981. JACM. Peterson, Gerald E.. Stickel, Mark E. PDF behind paywall.
- On word problems in equational theories. 1987. INRIA. Rusinowitch, Michael. Hsiang, Jieh. https://hal.archives-ouvertes.fr/inria-00075875/document
- Equations and rewrite rules. 1980. Stanford U CSD. Huet, Gerard. Oppen, Derek C.. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.397.599&rep=rep1&type=pdf
- Completion of a Set of Rules Modulo a Set of Equations. 1986. SIAM J. Comp. Jouannaud, Jean-Pierre. Kirchner, Helene. PDF behind paywall.

### Complexity and expressibility of unification and completion

- The undecidability of the third order dyadic unification problem. 1978. Information and Control. Baxter, Lewis Denver. https://www.sciencedirect.com/science/article/pii/S0019995878901729
- The undecidability of the third order second degree unification problem. 1976. York University CS Dept. Baxter, Lewis Denver. No PDF found online
- Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems. 1990. Information and Computation. Dauchet, Max. Heuillard, T, Lescanne, P, Tison, S. http://www.sciencedirect.com/science/article/pii/089054019090015A
- Rigid E-unification is NP-complete. 1988. Symposium on Logic in Computer Science. Gallier, J.. Snyder, W., Narandran, P., Plaisted, D. PDF behind paywall
- The undecidability of the second-order unification problem. 1981. Theoretical Computer Science. Goldfarb, Warren D. https://www.sciencedirect.com/science/article/pii/0304397581900402
- The connection between Hilbert’s tenth problem and systems of equations between words and lengths. 1967. Leningrad seminar on constructive mathematics. Matiyasevich, Yuri V. No PDF found online
- Enumerable sets are diophantine. 1970. Dokl. Akad. Nauk SSSR. Matiyasevich, Yuri V. No PDF found online
- The undecidability of the DA-unification problem. 1989. Journal of Symbolic Logic. Siekmann, J. Szabo, P. https://www.jstor.org/stable/2274856?seq=1#page_scan_tab_contents
- On the arithmetic inexpressiveness of term rewriting systems. 1988. 3rd IEEE LICS. Vorobyov, Sergey G. http://www.dbai.tuwien.ac.at/staff/vorobyov/lics88.pdf
- The complexity of unification. 1977. U. of Waterloo Math Dept. Baxter, Lewis Denver. https://cs.uwaterloo.ca/research/tr/1977/CS-77-25.pdf