Name
Abstract | ||
|---|---|---|
An inductive proof attempt may fail as the available induction hypotheses cannot be applied to simplify the conclusion. One of the major problems which arise when performing inductive proofs is to transform the conclusion of an induction step in order to make the hypothesis applicable. Often, to overcome this problem, several additional lemmae are needed. However, most inductive theorem provers rely upon user intervention in supplying the required lemmae. In contrast, we present a method for generating automatically lemmae. Generation of lemmae is motivated by attempts to find appropriate instantiations for non-induction variables in the inductive step. We consider implicative formulae of the form ∀x-yΓ(x-,y-) ← Δ(x-), where Γ and Δ are conjunction of atoms and x- and y- are vectors of universal and of existential variables respectively. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.ins.2003.06.012 | Inf. Sci. |
Keywords | Field | DocType |
appropriate instantiations,induction step,inductive proof attempt,inductive theorem provers,appropriate lemmae discovery,additional lemmae,available induction,inductive proof,existential variable,required lemmae,inductive step,mathematical induction,automated theorem proving,theorem prover | Theorem provers,Discrete mathematics,Program synthesis,Of the form,Automated theorem proving,Mathematical induction,Mathematical proof,Mathematics | Journal |
Volume | Issue | ISSN |
163 | 4 | 0020-0255 |
Citations | PageRank | References |
0 | 0.34 | 8 |
Authors | ||
2 | ||