音楽の論理とその機械化

• Item type: SIG Technical Reports(1)
• 公開日: 1994-08-06
• タイトル: 音楽の論理とその機械化
• タイトル / 言語: en
• タイトル: Logic of Music and its Mechanization
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: （株）富士通研究所情報社会科学研究所
• 著者所属(英): en
• 著者所属(英): Institute for Social Information Science (ISIS), FUJITSU LABORATORIES LTD.
• 著者名: 沢村, 一
• 著者名(英): Hajime, Sawamura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 高階論理定理証明機HOLは数学，プログラムの論理など人間の合理的思考に関わる厳密科学に対して適用されてきた．本論文では，HOL定理証明機の他の方向の応用として，人間の感性に関わる領域，特に音楽への応用を探求する．先ず，音楽について論じたり音楽を論理的かつ形式的に作曲するための基礎となる論理体系を提案する．これは音楽理論に関するこれまでの二つの研究：KurkelaのMontagueの内包論理による音楽の論理分析とKasslerのSchoenbergの12音音楽に対する論理体系，に基づいて形式化された．次に，このような音楽の論理における論証／計算を機械的に遂行するために，HOL定理証明機の上あるいは中に埋め込む方法を与えた．これらによって，音楽活動を定理の証明プロセスと見るこれまでとは異なった新しい視点がありうることを明らかにした．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10438388
• 書誌情報: 情報処理学会研究報告音楽情報科学（MUS）; 巻 1994, 号 71(1994-MUS-007), p. 23-30, 発行日 1994-08-06
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会