@article{oai:nagoya.repo.nii.ac.jp:00013079,
 author = {KUSAKARI, Keiichirou and CHIBA, Yuki},
 issue = {4},
 journal = {IEICE transactions on information and systems},
 month = {Apr},
 note = {The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming languages. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. A TRS cannot, however, directly handle higher-order functions that are widely used in functional programming languages. In this paper, we propose a higher-order KB procedure that extends the KB procedure to the framework of a simply-typed term rewriting system (STRS) as an extended TRS that can handle higher-order functions. We discuss the application of this higher-order KB procedure to a certification technique called inductionless induction used in program verification, and its application to fusion transformation, a typical kind of program transformation.},
 pages = {707--715},
 title = {A Higher-Order Knuth-Bendix Procedure and Its Applications},
 volume = {E90-D},
 year = {2007}
}