<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

Published Online: Dec 30, 2015

Page range: 130 - 149

Received: May 18, 2015

Accepted: Nov 19, 2015

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

Keywords
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

Published Online: Dec 30, 2015

Page range: 130 - 149

Received: May 18, 2015

Accepted: Nov 19, 2015

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

Keywordsmathematical 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.

Keywords
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