Mathematical Induction in Otter-lambda. Beeson, M. Journal of Automated Reasoning, 36(4):311-344, 2006.  
Pdf  bibtex   @article{beeson2006,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:07:51 +0000},
	date-modified = {2014-11-14 18:30:04 +0000},
	journal = {Journal of Automated Reasoning},
	keywords = {Automated deduction},
	number = {4},
	pages = {311-344},
	title = {Mathematical Induction in {O}tter-lambda},
	url_pdf = {induction.pdf},
	volume = {36},
	year = {2006}} 
Downloads: 0
{"_id":"n3TwsmXuAmEgWzb3h","bibbaseid":"beeson-mathematicalinductioninotterlambda-2006","author_short":["Beeson, M."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Michael"],"propositions":[],"lastnames":["Beeson"],"suffixes":[]}],"date-added":"2014-11-13 23:07:51 +0000","date-modified":"2014-11-14 18:30:04 +0000","journal":"Journal of Automated Reasoning","keywords":"Automated deduction","number":"4","pages":"311-344","title":"Mathematical Induction in Otter-lambda","url_pdf":"induction.pdf","volume":"36","year":"2006","bibtex":"@article{beeson2006,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:07:51 +0000},\n\tdate-modified = {2014-11-14 18:30:04 +0000},\n\tjournal = {Journal of Automated Reasoning},\n\tkeywords = {Automated deduction},\n\tnumber = {4},\n\tpages = {311-344},\n\ttitle = {Mathematical Induction in {O}tter-lambda},\n\turl_pdf = {induction.pdf},\n\tvolume = {36},\n\tyear = {2006}}\n\n","author_short":["Beeson, M."],"key":"beeson2006","id":"beeson2006","bibbaseid":"beeson-mathematicalinductioninotterlambda-2006","role":"author","urls":{" pdf":"http://www.michaelbeeson.com/research/papers/induction.pdf"},"keyword":["Automated deduction"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://www.michaelbeeson.com/research/papers/beeson.bib","dataSources":["v9esbf6gQ8h64d3NA"],"keywords":["automated deduction"],"search_terms":["mathematical","induction","otter","lambda","beeson"],"title":"Mathematical Induction in Otter-lambda","year":2006}