Christopher Lynch

Rewriting in theorem proving

Christopher Lynch (Clarkson University, USA)

Please find some material here.

Rewriting techniques are important tools for reasoning about equality in first-order theorem proving. This lecture will explain how rewriting techniques are incorporated into first-order 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 first-order logic, and then to first-order logic with equality, showing how difierent theorem proving strategies are based on the fundamentals of selection rules and redundancy. We will explain the model-construction 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 E-unification. This is then lifted to basic paramodulation for first-order theorem proving.
Finally we move to exciting new results on rewriting modulo background theories. We survey some recent results on techniques for E-unification 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 E-unification, 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

  1. Theorem Proving in Propositional Logic

    1. Conversion to Clauses
    2. Resolution Inference Rules
    3. Soundness and Completeness results
    4. Subsumption
    5. Tautology Deletion
    6. Redundancy (an abstract notion)
    7. Ordered Resolution
    8. Selection Rules
  2. Theorem Proving in First Order Logic

    1. Conversion to Clauses
    2. Resolution Inference Rules
    3. Soundness and Completeness results
    4. Subsumption
    5. Tautology Deletion
    6. Redundancy (an abstract notion)
    7. Properties of Orderings
    8. Ordered Resolution
    9. Selection Rules
  3. Theorem Proving in First Order Logic with Equality

    1. Conversion to Clauses
    2. Axiomatizing Equality
    3. Paramodulation Inference Rules
    4. Soundness and Completeness results
    5. Subsumption
    6. Tautology Deletion
    7. Demodulation
    8. Redundancy (an abstract notion)
    9. Properties of Orderings
    10. Superposition (not Ordered Paramodulation)
    11. Selection Rules
  4. Proving Completeness using Model Construction

    1. Model Construction for Propositional Logic
    2. Model Construction for First Order Logic
    3. Model Construction for First Order Logic with Equality
  5. E-unification in Rewrite Theories

    1. Word problem viewed as Superposition
    2. E-Unification
    3. Narrowing
    4. Basic Narrowing
    5. The Forward Overlap rule
    6. Deciding E-Unification using Basic Narrowing
    7. Basic Completion
    8. Basic Paramodulation
    9. Selection rules
    10. Redundancy
  6. E-Unification in Specialized Theories

    1. Inference Rules for Syntactic Unification
    2. Extending to Equational Theories
    3. Associativity and Commutativity
    4. Associativity
    5. Exclusive OR with Homomorphism
  7. E-Unification in Rewrite Theories modulo Equational Theories

    1. Narrowing
    2. The Extension Rule
    3. Basic Narrowing
    4. The Parallel rule
    5. The Forward Overlap rule
    6. Deciding E-Unification using Basic Narrowing modulo
    7. Interesting Examples
    8. Basic Completion modulo
    9. Basic Paramodulation modulo
    10. Selection rules
    11. Redundancy

Exercises or experiments

There will be exercises for students to work on.

Bibliographical references

  1. Franz Baader and Wayne Snyder. Unifiation theory. In Robinson and Voronkov [14], pages 445–532.
  2. Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theor. Comput. Sci., 67(2&3):173–201, 1989.
  3. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Robinson and Voronkov [14], pages 19–99.
  4. Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Inf. Comput., 121(2):172–192, 1995.
  5. Alan Bundy, editor. Automated Deduction – CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 – July 1, 1994, Proceedings, volume 814 of Lecture Notes in Computer Science. Springer, 1994.
  6. Dohan Kim, Christopher Lynch, and Paliath Narendran. Basic paramodulation modulo an equational theory revisited, 2019.
  7. Dohan Kim, Christopher Lynch, and Paliath Narendran. Redeeming basic narrowing modulo, 2019.
  8. Zhiqiang Liu and Christopher Lynch. Efficient general agh-unification. Inf. Comput., 238:128–156, 2014.
  9. Christopher Lynch. Constructing Bachmair-Ganzinger models. In Voronkov and Weidenbach [16], pages 285–301.
  10. Robert Nieuwenhuis. Decidability and complexity analysis by basic paramodulation. Inf. Comput., 147(1):1–21, 1998.
  11. Robert Nieuwenhuis and Albert Rubio. AC-superposition with constraints: No ac-unifiers needed. In Bundy [5], pages 545–559.
  12. Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In Robinson and Voronkov [14], pages 371–443.
  13. Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233–264, 1981.
  14. John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001.
  15. Michaëel Rusinowitch and Laurent Vigneron. Automated deduction with associative-commutative operators. Appl. Algebra Eng. Commun. Comput., 6:23–56, 1995.
  16. Andrei Voronkov and Christoph Weidenbach, editors. Programming Logics – Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Computer Science. Springer, 2013.

Comments are closed.