image part 004

Automated Reasoning

Another area of interest is automated reasoning, i.e., algorithms for proving and disproving mathematical statements. In certain cases, solving reasoning tasks is an end in itself. In other cases, automated reasoning is a tool for establishing that a system is safe or inferring useful facts that can aid learning and program synthesis. In either case, the computational complexity of exploring spaces of proofs and counterexamples is a formidable barrier. As with program synthesis, we approach this challenge by complementing classical automated reasoning techniques with contemporary statistical learning methods.