author = {Tudor Jebelean},
title = {{Algebraic Methods in Automated Reasoning}},
language = {english},
abstract = {We present succintly a case study on automatic generation of natural--style proofs in elementary analysis, by employing algorithms from computer algebra. In order to produce proofs which are similar to those realized by human mathematicians, we use a system similar to sequent calculus, in which the most difficult steps consist in finding the witness terms for the existential goals and the instantiation terms for the universal assumptions. We study how these can be found by using computer algebra algorithms, and what are the current limitations and perspectives of this approach.},
year = {2017},
month = {June 29},
note = {Invited talk at 4th Conference of Mathematical Society of the Republic of Moldova},
keywords = {computer algebra, natural-style proving},
sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
conferencename = {4th Conference of Mathematical Society of the Republic of Moldova},
url = {http://cmsm4.math.md}