Rewriting in theorem provingChristopher Lynch (Clarkson University, USA) 
Please find some material here.
Rewriting techniques are important tools for reasoning about equality in firstorder theorem proving. This lecture will explain how rewriting techniques are incorporated into firstorder theorem provers. We will start from the basics and slowly work our way up to the modern theory of rewriting in theorem proving.
We begin the lecture with classical results on theorem proving, based on resolution and paramodulation. We start with propositional logic, work our way up to firstorder logic, and then to firstorder logic with equality, showing how difierent theorem proving strategies are based on the fundamentals of selection rules and redundancy. We will explain the modelconstruction technique for proving completeness of paramodulation, again building our way up from the simple to the complex.
Next we move to more modern topics of dealing with equality efficiently in theorem proving. We start with the topic of narrowing, then the more efficient strategy of basic narrowing, which the rest of the lecture will be based on. We show how basic narrowing can be used as a decision procedure for Eunification. This is then lifted to basic paramodulation for firstorder theorem proving.
Finally we move to exciting new results on rewriting modulo background theories. We survey some recent results on techniques for Eunification in specialized theories, using inference rules. Then we move into narrowing modulo equational theories. We give some new results on basic narrowing modulo equational theories, show how it can be used to decide Eunification, and then lift that to new results on basic paramodulation modulo equational theories.
This will cover two slots. The first slot will give the classical results of rewriting in theorem proving. The second slot will detail the exciting new techniques
involving theorem proving modulo and equational theory.
Outline of the lecture

Theorem Proving in Propositional Logic
 Conversion to Clauses
 Resolution Inference Rules
 Soundness and Completeness results
 Subsumption
 Tautology Deletion
 Redundancy (an abstract notion)
 Ordered Resolution
 Selection Rules

Theorem Proving in First Order Logic
 Conversion to Clauses
 Resolution Inference Rules
 Soundness and Completeness results
 Subsumption
 Tautology Deletion
 Redundancy (an abstract notion)
 Properties of Orderings
 Ordered Resolution
 Selection Rules

Theorem Proving in First Order Logic with Equality
 Conversion to Clauses
 Axiomatizing Equality
 Paramodulation Inference Rules
 Soundness and Completeness results
 Subsumption
 Tautology Deletion
 Demodulation
 Redundancy (an abstract notion)
 Properties of Orderings
 Superposition (not Ordered Paramodulation)
 Selection Rules

Proving Completeness using Model Construction
 Model Construction for Propositional Logic
 Model Construction for First Order Logic
 Model Construction for First Order Logic with Equality

Eunification in Rewrite Theories
 Word problem viewed as Superposition
 EUnification
 Narrowing
 Basic Narrowing
 The Forward Overlap rule
 Deciding EUnification using Basic Narrowing
 Basic Completion
 Basic Paramodulation
 Selection rules
 Redundancy

EUnification in Specialized Theories
 Inference Rules for Syntactic Unification
 Extending to Equational Theories
 Associativity and Commutativity
 Associativity
 Exclusive OR with Homomorphism

EUnification in Rewrite Theories modulo Equational Theories
 Narrowing
 The Extension Rule
 Basic Narrowing
 The Parallel rule
 The Forward Overlap rule
 Deciding EUnification using Basic Narrowing modulo
 Interesting Examples
 Basic Completion modulo
 Basic Paramodulation modulo
 Selection rules
 Redundancy
Exercises or experiments
There will be exercises for students to work on.
Bibliographical references
 Franz Baader and Wayne Snyder. Unifiation theory. In Robinson and Voronkov [14], pages 445–532.
 Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theor. Comput. Sci., 67(2&3):173–201, 1989.
 Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Robinson and Voronkov [14], pages 19–99.
 Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Inf. Comput., 121(2):172–192, 1995.
 Alan Bundy, editor. Automated Deduction – CADE12, 12th International Conference on Automated Deduction, Nancy, France, June 26 – July 1, 1994, Proceedings, volume 814 of Lecture Notes in Computer Science. Springer, 1994.
 Dohan Kim, Christopher Lynch, and Paliath Narendran. Basic paramodulation modulo an equational theory revisited, 2019.
 Dohan Kim, Christopher Lynch, and Paliath Narendran. Redeeming basic narrowing modulo, 2019.
 Zhiqiang Liu and Christopher Lynch. Efficient general aghunification. Inf. Comput., 238:128–156, 2014.
 Christopher Lynch. Constructing BachmairGanzinger models. In Voronkov and Weidenbach [16], pages 285–301.
 Robert Nieuwenhuis. Decidability and complexity analysis by basic paramodulation. Inf. Comput., 147(1):1–21, 1998.
 Robert Nieuwenhuis and Albert Rubio. ACsuperposition with constraints: No acunifiers needed. In Bundy [5], pages 545–559.
 Robert Nieuwenhuis and Albert Rubio. Paramodulationbased theorem proving. In Robinson and Voronkov [14], pages 371–443.
 Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233–264, 1981.
 John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001.
 Michaëel Rusinowitch and Laurent Vigneron. Automated deduction with associativecommutative operators. Appl. Algebra Eng. Commun. Comput., 6:23–56, 1995.
 Andrei Voronkov and Christoph Weidenbach, editors. Programming Logics – Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Computer Science. Springer, 2013.