@techreport{oai:ipsj.ixsq.nii.ac.jp:00056531,
 author = {沢村, 一 and Hajime, Sawamura},
 issue = {71(1994-MUS-007)},
 month = {Aug},
 note = {高階論理定理証明機HOLは数学，プログラムの論理など人間の合理的思考に関わる厳密科学に対して適用されてきた．本論文では，HOL定理証明機の他の方向の応用として，人間の感性に関わる領域，特に音楽への応用を探求する．先ず，音楽について論じたり音楽を論理的かつ形式的に作曲するための基礎となる論理体系を提案する．これは音楽理論に関するこれまでの二つの研究：KurkelaのMontagueの内包論理による音楽の論理分析とKasslerのSchoenbergの12音音楽に対する論理体系，に基づいて形式化された．次に，このような音楽の論理における論証／計算を機械的に遂行するために，HOL定理証明機の上あるいは中に埋め込む方法を与えた．これらによって，音楽活動を定理の証明プロセスと見るこれまでとは異なった新しい視点がありうることを明らかにした．, HOL(Higher-Order Logic Theorem Prover) has been mainly applied to exact sciences such as mathematics and logics of programs in which human's rational thinking is actively engaged. As another direction of applications of the HOL theorem prover, we explore arts which is involved in human emotion, in particular, music. First, we present a logical music system which is supposed to be an underlying logic for both reasoning about music and composing music. This is based on two previous work on music theory in which logic plays a key role: Kurkela's semantical analysis of music based on Montague's intensional logic and Kassler's logical system for Schoenberg's twelve-tone music. Next, a mechanization of such a logical music system is provided very smoothly by using the expressiveness and proof facilities of HOL and by programming ML functions representing the symbol manipulations to be needed in the logical music system. We believe that in the future, theorem proving technology would help human's emotional activities as well, in addition to human's rational information processing. This paper may be viewed as a first attempt toward relating music to logic in the area of automated theorem proving.},
 title = {音楽の論理とその機械化},
 year = {1994}
}