Bibliography

Arts T, Giesl J. Automatically proving termination where simplification orderings fail. In: TAPSOFT: 7th International Joint Conference on Theory and Practice of Software Development. Springer-Verlag; 1997:261–272. LNCS 1214.

Baader F, Snyder W. Unification theory. chapter 8 In: Robinson A, Voronkov A, eds. Elsevier Science; 445–532. Handbook of Automated Reasoning. 2001;Vol. I.

Bachmair L. Proof normalization for resolution and paramodulation. In: Third int. conf. on Rewriting Techniques and Applications (RTA). Springer-Verlag; 1989:15–28. LNCS 355.

Bachmair L. Canonical equational proofs. Chapel Hill, NC, USA: Birkhäuser; 1991.

Bachmair L, Dershowitz N. Completion for rewriting modulo a congruence. Theoretical Computer ...

Get Handbook of Automated Reasoning now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial