Update: Jul 22, 2016

PPDP 2016 Paper

Proving Inductive Validity of Constrained Inequalities

Takahiro Nagao and Naoki Nishida
In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016),
Edinburgh, United Kingdom, September 2016.
Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Within the framework, we handle inequalities that may contain function symbols defined in a given rewriting system but not necessarily interpreted by the built-in semantics. Direct handling of inequalities facilitates the utilization of transitivity of magnitude relations via inequalities obtained as induction hypotheses. Our approach succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations.
[DOI: 10.1145/2967973.2968598] [pre-print] [proofs]

Sakai Lab. Graduate School of Informatics Dept. of Information Engineering Graduate School/School of Engineering Nagoya University
Produced by N.Nishida (nishida @ i.nagoya-u.ac.jp)