2010/10/30 by Rina Panigrahy, Panigrahy, Rina
Computer Science · #Computability, Logic, AI Algorithms #Logic, programming, and type systems #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.1011.0046
The paper explores known results related to the problem of identifying if a\ngiven program terminates on all inputs -- this is a simple generalization of\nthe halting problem. We will see how this problem is related and the notion of\nproof verifiers. We also see how verifying if a program is terminating involves\nreasoning through a tower of axiomatic theories -- such a tower of theories is\nknown as Turing progressions and was first studied by Alan Turing in the\n1930's. We will see that this process has a natural connection to ordinal\nnumbers. The paper is presented from the perspective of a non-expert in the\nfield of logic and proof theory.\n