Part of the CLAS 2022 |

Site Search

THEOREM PROVING WITH APPLICATIONS

Christopher Lynch Christopher Lynch (Clarkson University)

Abstract

Rewriting techniques are important tools for reasoning about equality in automated theorem provers. 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 different 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.

We discuss how these techniques can be applied to SMT solvers, and we present ongoing work on how to use the above ideas for quantifier instantiation and model representation.

Next we move to 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 most of 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 can be lifted to basic paramodulation for first-order theorem proving.

Then we discuss some fairly new results on rewriting modulo background theories. Narrowing can be performed 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.

We survey some recent results on techniques for E-unification in specialized theories, using inference rules. Then we apply this work to the topic of the synthesis of cryptographic algorithm, showing how to use E-unification for security and authentication of modes of encryption.

This will cover two slots. The first slot will give the classical results of theorem proving, and the new work on applying these techniques to Satisfiability Modulo Theories. The second slot will detail new techniques on deciding E-unification using Narrowing modulo equational theories, plus the recent work on E-unification and synthesis of Cryptographic Modes of Operation.


Outline


1. Theorem Proving in Propositional Logic

2. Theorem Proving in First Order Logic

3. Theorem Proving in First Order Logic with Equality

4. Proving Completeness using Model Construction

5. Proving Completeness using Model Construction

6. E-unification in Rewrite Theories

7. E-Unification in Rewrite Theories modulo Equational Theories

8. E-Unification in Specialized Theories