User talk:Linket

From Wikipedia, the free encyclopedia
Jump to: navigation, search

Automated theorem proving[edit]

Hi Linket,

before we get into an edit war: Of course ATP systems can, in principle, try to prove that a program halts. They can even succeed in many cases (a simple case is e.g. proof by structural argument: A program terminates if there is no unbounded loop or general recursion in it). In fact, proving termination is a not insignificant subfield of automated reasoning[1], with it's own workshop series[2] and just to prove that it really works, a regular competition [3]. Gödel and Turing have shown that there are problems that cannot be solved or proven in any formal system, but that applies to humans as well as to automated theorem provers. Humans can change the paradigm, but there is nothing that forbids ATP system from doing the same (and, with proof assistants, that is often what happens). You want to write that "ATP is a subfield [...] dealing with proving a limited set of mathematical theorems". But the field is not limited in that way. Our programs are, but then they are constantly evolving to become more powerful. Compare "Physics is the natural science that involves the study of matter and its motion through space and time, along with related concepts such as energy and force." We don't understand all of physical reality, but physics is the field that that tries to understand more and more of it. ATP as a field cannot prove all mathematical theorems, but we are sure trying to solve more and more of them. --Stephan Schulz (talk) 08:02, 8 March 2014 (UTC)