Decision Procedures and Inductive Proofs Using Equational Logic
Janees E K,
M.Tech,
02,
81 pp.
Department of
Computer Science and Engineering
Indian Institute of Technology Bombay,
Powai, Mumbai 400 076.
Supervisor(s):
G.Sivakumar
Decision procedures are algorithms to check the validity or
satisfiability of a class of formulas in a given theory. They always terminate with a positive
or negative answer. Such algorithms are used for reasoning in many computer
applications, including symbolic algebraic computation, automated theorem
proving, program specification and verification, and high-level programming
languages
Presburger arithmetic or linear arithmetic is one such decidable theory that
deals with those equation that can be build up from integer constants, integer
variables, addition and mathematical relation like greater-than less-than, equal
Application of this theory include analysing data dependencies in optimizing
compilers and hardware verification.
The complexity of any decision procedure for Presburger Arithmetic is super
exponential. Best known algorithm for full theory is by Cooper, but it is very
inefficient in practice. A semi-decision procedure described by Shostak uses
Bledose's SUP-INF method. This method has exponential ($2^n$) complexity
on the size of equation for subclass theory whose variables are universally
quantified.
In this project, We worked on universally quantified extended Presburger
arithmetic which has un-interpreted functions. Shostak's method is used to decid
the validity of the equation. This involves replacing functions with variables a
finding contradiction for the equations to be proved.
We also explored functions that are defined recursively. Such functions are
solved employing cover-set method proposed by Deepak Kapur and Hanto
Zhang. This involves creating inductive hypothesis from the set of equation
defining the function and conjecture to be proved. These hypothesis are proved
by using Presburger arithmetic, rewriting and semantic unification.
We implemented this in LISP as part of Rewrite Rule Laboratory (RRL), a theorem
which uses rewrite technique