Music and mathematics have a long-standing relationship, but what about music and logic? Only recently have some authors started to explore the relationship between logic and music analysis, thanks to developments in both fields. The aim of this paper is to analyze this relationship, by developing a system capable of analyzing chord sequences using a logical presentation as well as create new harmonic structures. The logical presentation draws heavily from proof theory and its dual, i.e. tableuax. Also if music is not a proof, its adaptability makes it effective for this purpose. The attempt here proposed will try to apply proof theory to a brief, but important part of music: chord sequence analysis.