<abstract xmlns="http://www.w3.org/1999/xhtml"><p>This paper outlines a logical representation of certain aspects of the process of mathematical proving that are important from the point of view of Artificial Intelligence. Our starting-point is the concept of <italic>proof-event</italic> or <italic>proving</italic>, introduced by Goguen, instead of the traditional concept of mathematical proof. The reason behind this choice is that in contrast to the traditional static concept of mathematical proof, proof-events are understood as processes, which enables their use in Artificial Intelligence in such contexts, in which problem-solving procedures and strategies are studied.</p><p>We represent proof-events as problem-centered spatio-temporal processes by means of the language of the calculus of events, which captures adequately certain temporal aspects of proof-events (i.e. that they have <italic>history</italic> and form <italic>sequences of proof-events</italic> evolving in time). Further, we suggest a “loose” semantics for the proof-events, by means of Kolmogorov’s calculus of problems. Finally, we expose the intented interpretations for our logical model from the fields of automated theorem-proving and Web-based collective proving.</p></abstract>

This paper outlines a logical representation of certain aspects of the process of mathematical proving that are important from the point of view of Artificial Intelligence. Our starting-point is the concept of proof-event or proving, introduced by Goguen, instead of the traditional concept of mathematical proof. The reason behind this choice is that in contrast to the traditional static concept of mathematical proof, proof-events are understood as processes, which enables their use in Artificial Intelligence in such contexts, in which problem-solving procedures and strategies are studied.We represent proof-events as problem-centered spatio-temporal processes by means of the language of the calculus of events, which captures adequately certain temporal aspects of proof-events (i.e. that they have history and form sequences of proof-events evolving in time). Further, we suggest a “loose” semantics for the proof-events, by means of Kolmogorov’s calculus of problems. Finally, we expose the intented interpretations for our logical model from the fields of automated theorem-proving and Web-based collective proving.

On Mathematical Proving<xref ref-type="fn" rid="fn1_w2aab2b8c13b1b7b1ab1aaAa"/>

National Technical University of Athens, School of Applied Mathematical and Physical Sciences

The Hellenic Open University, School of Humanities

Journal of Artificial General Intelligence

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

This paper outlines a logical representation of certain aspects of the process of mathematical proving that are important from the point of view of Artificial...

On Mathematical Proving

Publicado en línea: 30 dic 2015

Páginas: 130 - 149

Recibido: 18 may 2015

Aceptado: 19 nov 2015

DOI: https://doi.org/10.1515/jagi-2015-0007

Palabras clave
mathematical proof, proof-event, problem solving, agents, calculus of events, Kolmogorov’s calculus of problems, Polymath project, T. Gowers, J. Goguen, R. Kowalski, A.N. Kolmogorov

© 2015 Petros Stefaneas et al., published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

On Mathematical Proving

Publicado en línea: 30 dic 2015

Páginas: 130 - 149

Recibido: 18 may 2015

Aceptado: 19 nov 2015

DOI: https://doi.org/10.1515/jagi-2015-0007

Palabras clavemathematical proof, proof-event, problem solving, agents, calculus of events, Kolmogorov’s calculus of problems, Polymath project, T. Gowers, J. Goguen, R. Kowalski, A.N. Kolmogorov

© 2015 Petros Stefaneas et al., published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
mathematical proof, proof-event, problem solving, agents, calculus of events, Kolmogorov’s calculus of problems, Polymath project, T. Gowers, J. Goguen, R. Kowalski, A.N. Kolmogorov