Some applications of Gentzen's proof theory to automated deduction. Beeson, M. In Extensions of Logic Programming, volume 475, of Lecture Notes in Computer Science, pages 101-156. Springer-Verlag, 1991.  
Pdf  bibtex   @incollection{beeson1991,
	author = {Michael Beeson},
	booktitle = {Extensions of Logic Programming},
	date-added = {2014-11-14 21:57:08 +0000},
	date-modified = {2019-10-15 11:47:36 -0700},
	editor = {P. Schroeder-Heister},
	keywords = {Proof theory, Automated deduction},
	pages = {101-156},
	publisher = {Springer-Verlag},
	series = {Lecture Notes in Computer Science},
	title = {Some applications of {G}entzen's proof theory to automated deduction},
	url_pdf = {Gentzen.pdf},
	volume = {475},
	year = {1991}} 
Downloads: 0
{"_id":"tqQdpSCvhrPtsXJri","bibbaseid":"beeson-someapplicationsofgentzensprooftheorytoautomateddeduction-1991","author_short":["Beeson, M."],"bibdata":{"bibtype":"incollection","type":"incollection","author":[{"firstnames":["Michael"],"propositions":[],"lastnames":["Beeson"],"suffixes":[]}],"booktitle":"Extensions of Logic Programming","date-added":"2014-11-14 21:57:08 +0000","date-modified":"2019-10-15 11:47:36 -0700","editor":[{"firstnames":["P."],"propositions":[],"lastnames":["Schroeder-Heister"],"suffixes":[]}],"keywords":"Proof theory, Automated deduction","pages":"101-156","publisher":"Springer-Verlag","series":"Lecture Notes in Computer Science","title":"Some applications of Gentzen's proof theory to automated deduction","url_pdf":"Gentzen.pdf","volume":"475","year":"1991","bibtex":"@incollection{beeson1991,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Extensions of Logic Programming},\n\tdate-added = {2014-11-14 21:57:08 +0000},\n\tdate-modified = {2019-10-15 11:47:36 -0700},\n\teditor = {P. Schroeder-Heister},\n\tkeywords = {Proof theory, Automated deduction},\n\tpages = {101-156},\n\tpublisher = {Springer-Verlag},\n\tseries = {Lecture Notes in Computer Science},\n\ttitle = {Some applications of {G}entzen's proof theory to automated deduction},\n\turl_pdf = {Gentzen.pdf},\n\tvolume = {475},\n\tyear = {1991}}\n\n","author_short":["Beeson, M."],"editor_short":["Schroeder-Heister, P."],"key":"beeson1991","id":"beeson1991","bibbaseid":"beeson-someapplicationsofgentzensprooftheorytoautomateddeduction-1991","role":"author","urls":{" pdf":"http://www.michaelbeeson.com/research/papers/Gentzen.pdf"},"keyword":["Proof theory","Automated deduction"],"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"http://www.michaelbeeson.com/research/papers/beeson.bib","dataSources":["v9esbf6gQ8h64d3NA"],"keywords":["proof theory","automated deduction"],"search_terms":["applications","gentzen","proof","theory","automated","deduction","beeson"],"title":"Some applications of Gentzen's proof theory to automated deduction","year":1991}