Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

Hirotaka Koike

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 15, 1999

Keywords: inductionless induction ,rewriting induction ,automated theorem proving

, term rewriting system.

The properties of systems based on equation such as functional programming and

algebraic sp ecication are often treated as inductive theorems in equational reasoning.

Therefore, automated theorem proving of inductive theorems in equational reasoning

is indispensable to the automated verication of functional programming and algebraic

specications.

Automated inductivetheorem provingisclassiedintoexplicit inductionand implicit

induction. Explicit induction isthe methodusing inductive schemedirectly. The Nqthm

system, develop ed withinthis framework,isconsidered asone ofthe most successfulthe-

orem provers. On the other hand, implicit induction is the methods proving inductive

theorems without the explicit use of induction scheme. There exist inductionlessinduc-

tion and rewriting induction as implicitinduction. Inductionless induction wasproposed

by Musser(1980) and was rened in Huet and Hullot(1982). Rewriting induction was

proposed by Reddy(1990). RRL and SPIKE are well-known automated theorem provers

based oninductionless induction and rewriting induction, respectively.

Implicit induction methods proveinductivetheorems as follows: LetE bean axiom

and e = e 0

the equation to b e proven. By adding e = e 0

to E, we can obtain another

system E 0

= E [fe = e 0

g. The next step is to show that two congruence relations

generated by E and E 0

are the same onground terms. If this step succeeds, e =e 0

is an

inductivetheorem inE, since obviouslye =e 0

is an inductive theorem in E 0

. Thus, it is

shown that e=e 0

is aninductive theorem inE withoutthe explicit use of mathematical

induction.

Knuth-Bendix completion, cover set and test set techniques are used in automated

theorem provers based on inductionless induction or rewriting induction. Therefore, in-

ductionlessinduction andrewritinginduction areoftenstudiedasanextensionofKnuth-

Bendixcompletiontechniquesorinductionbasedoncoverset(testset). However,essence

Copyright c

1999byHirotakaKoike

tion technique or coverset (test set) techniques are not essential. In fact,Toyama(1991)

removes the concept of completion and reconstructs the inductionless induction in the

framework of abstract reduction systems. Consequently, it was shown that the Church-

Rosserpropertyandtheweaknormalizationpropertyareessentialininductionlessinduc-

tion.

In this paper, we study the relation b etween inductionless induction and rewriting

induction within anabstract framework asfollows:

Formalizationof rewriting induction

We reconstruct the rewriting induction methods in the ame work of abstract re-

ductionsystems. We clearly showthat the regression property and the strong nor-

malization property are essential in rewriting induction. The principle of rewriting

induction can be concisely explainedby our result.

Comparison between inductionless induction and rewriting induction

Fromtheab overesult,itispossibletocompareinductionlessinductionandrewriting

inductioninauniformabstractframework. WemakeitclearthattheChurch-Rosser

prop erty and the reachability are essential in inductionless induction while the re-

gression property and the strong normalization property are essential in rewriting

induction. Thus,twomethodsare incompatible.

Comparison with refutationalytheorem proving

In the similar way, we also study refutationaly proving that is widely used in au-

tomated theorem provers. Consequently, weshow thatunder thecombinationwith

refutaional proving inductionlessinduction and rewriting induction coincide.

Relationship with automatedtheorem provers

We consider the relation between automated theorem provers and our abstract

framework. In this paper, we deal with Kapur's procedure as inductionless in-

duction and Frib ourg's procedure as rewriting induction. Both procedures prove

as follows: Let a TRS R

1

be an axiom and e ! e 0

a rule that corresponds to

an equation to be proven. In the rst step, by adding e ! e 0

to R

1

, we obtain

R

2

=R

1

[fe !e 0

g. Next, we transform R

2

intothe TRS that meets suitablecon-

ditions with procedures based on Knuth-Bendix completion. When the procedure

halts,theresultedTRShaspropertiesinourabstractframework. Thus,mechanisms

of automated theorem proversare explained concisely.

Wegeneralize the metho dstoshowequivalenceof twosystemswithinabstract reduc-

tion systems. Our approach is eective for designing new automated theorem provers.

Furthermore, our metho ds can apply not only to inductive theorems but also to various

automated theorem provers.