Reasoning, Metareasoning, and Mathematical Truth: Studies of Theorem Proving under Limited Resources
This work addresses the challenge of making timely decisions in theorem proving under limited resources, which is incremental as it builds on prior methods for flexible inference and metareasoning.
The paper tackles the problem of inferring beliefs about mathematical truth before an automated theorem prover completes a proof, using Bayesian analysis to update beliefs based on progress and decision-theoretic methods to decide between continuing deliberation or taking immediate action in time-critical situations.
In earlier work, we introduced flexible inference and decision-theoretic metareasoning to address the intractability of normative inference. Here, rather than pursuing the task of computing beliefs and actions with decision models composed of distinctions about uncertain events, we examine methods for inferring beliefs about mathematical truth before an automated theorem prover completes a proof. We employ a Bayesian analysis to update belief in truth, given theorem-proving progress, and show how decision-theoretic methods can be used to determine the value of continuing to deliberate versus taking immediate action in time-critical situations.