Complete list of the
things to be discussed with J on Alan first set of correcctions.


page1:

-title:
First note that I have changed the title to the title of the arXiv publication 
"Automation of Mathematical Induction as part of the History of Logic"
because Alan has required to put a reference to the
history of logic into the abstract (instead of mentioning it first
in Section 2.) As there is no abstract intended in these handbook
articles, I think we have to - and should actually - mention this
reference somehow in the title. Note that Elsevier will sell our
article online without the handbook.

-Alan's remarks on evidence:
I do not think that we have to give evidence for our very well-justified
motivating judgements here (just because they could be misunderstood).
Moreover, I do think that initial paragraphs may use a sophisticated 
form of expression. 
So, contrary to the later pages where I followed Alan most carefully, 
I ignored most of Alan's remarks here
and added only the now TPTP-winning Satallax as another 
HO TP in the footnote on LEO-II.



page 2:

-3rd para:
You wrote:
"The work on this breakthrough in the automation of inductive theorem proving
was started quite deliberately in September 1972, by Robert S. Boyer and
J Strother Moore, in Edinburgh, Scotland."
Alan asks:
"What non-deliberate starting are you contrasting this with?"
I see neither a reason for a change, nor how this question could be answered.

-last para:
Alan writes about the first occurrence of the term "waterfall":
"The origins of this term lie in software engineering methodologies 
popular at the time. I think this deserves a mention."
I have added a footnote as follows:
"``waterfall''\footnote{%
 See \figuref{figure waterfall} for the \boyermoorewaterfall.
 See \cite{waterfall} for the probably first occurrence of 
 ``waterfall'' as a term in software engineering.}"
Is that OK with you? 

@Inproceedings{waterfall,
year={1976},
author={Thomas E. Bell 
    and T. A. Thayer},
title={Software Requirements: Are They Really a Problem?},
note={In \cite[\PP{61}{68}]{secondICSEseventysix}, \url{http://pdf.aminer.org/000/361/405/software_requirements_are_they_really_a_problem.pdf}},}
@Proceedings{secondICSEseventysix,
year={1976},
editor={Raymond T. Yeh 
    and C. V. Ramamoorthy},
title={\Proc\ \nth 2 \Int\ \Conf\ on Software Engineering, San Francisco (CA), \Oct\,13--15, 1976},
publisher={\ieeeCSpress},
note={\url{http://dl.acm.org/citation.cfm?id=800253}},}



page 26:

-1st line f.:
Alan asks to explain why there is this difference between human induction
and explicit induction. I can only state it as a matter of fact. Can you
or Bob give a hint here?

-4th para.
Our text is:
"Generalization is hardly needed when 
 input conjectures are supplied by humans."
Alan writes:
"That's not my experience. 
 Many human-supplied theorems require generalisation,
 i.e.,the conjecture has to be generalised before induction."
CP:
"This, however, is absolutely not my experience. 
 I often need new notions and lemmas,
 but it hardly happens that a conjecture I supply needs generalization.
 In QuodLibet this is switched off by default.
 What is your experience?"



page 28:

-Last sentence in item 2:
Contrary to Alan's suggestion,
I think we should not display the cut rule 
because a common misunderstanding is that the cut rule cannot be 
eliminated in induction,
whereas the hard result actually refers to the sub-formula property,
but not to the cut rule.

-Note 70:
Our text is:
"In practice, however, 
 we have to extend our proof search to 
 additional lemmas and notions anyway,
 and it does not really matter whether we have to do this 
 for principled reasons (as in induction) 
 or for tractability (as required in \firstorder\ deductive theorem proving,
 \cfnlb\ \cite{baazleitschcolllog})."
Alan writes:
"I disagree. I think this difference has a real practical impact."
CP:
"The practical impact seems to exist only because the whole TPTP
 community is trying to work with problems where the proof can be
 found without extending the language. The recent success of higher-order
 TPs in the TPTP results mostly from being able to provide the
 language extension required in practice. Baaz and Leitsch's paper
 is one of their strongest ones and provides strong evidence for 
 first-order logic at least."
Our new text is:
"In practice, 
 however, 
 proof search for harder theorems often requires 
 to express additional lemmas and notions,
 and it is only a matter of degree 
 whether we have to do this for principled reasons (as in induction) 
 or for tractability (as required in \firstorder\ deductive theorem proving,
 \cfnlb\ \cite{baazleitschcolllog})."
Is that OK with you?