Formalized Reasoning for Symbolic Music Representations
MIDI numbers treat D♯ and E♭ as identical, yet in music theory they are not the same note. This fundamental ambiguity undermines symbolic reasoning for interval spelling, chord spelling, and key transposition. Discover a formal specification written in Z notation that resolves the problem, and see how classic constructs—interval qualities, chord inversion, doubled notes—can be embedded into a computational knowledge base exactly as a trained musician would understand them.