Automated Reasoning and Data Mining

The planned research will be focused on the development and applications of automated theorem provers, formal theorem proving and data mining techniques. In the field of automated theorem proving, we plan to continue the development of the SAT solver ArgoSAT, to develop a novel SMT solver ArgoSMT and to develop a new prover for coherent logic ArgoCLP. Solvers ArgoSAT and ArgoSMT will be applied on solving important practical problems of planning, optimization and software verification. The ArgoCLP prover will be applied on formalization of geometry, on automated solving of constructive problems, and also within the geometry software GCLC. In the field of formal theorem proving, we plan to develop verified computer programs and to formalize some mathematical theories. We plan to develop and apply novel techniques for data mining, suitable for automated reasoning, but also for some other areas, most notably bioinformatics. These techniques will be used for improving efficiency and for evaluation of automated theorem provers, for analysis of genome and protein sequences and for prediction of some neurological diseases. We plan to publish and disseminate results of our research on major conferences and in journals, to organize scientific seminars, workshops and conferences, to maintain ongoing and to establish new collaborations with other researchers and research groups. The presented plan is a sequel of the research conducted within the current research grant 144030.