A theorem proving approach for automatically synthesizing visualizations of flow cytometry data