Studies of Theorem Proving under Limited Resources

Decision Theory Group
Microsoft Research
Redmond, Washington 98052-6399

Adrian Klein

Center for the Study of Language and Information
Stanford University
Ventura Hall
Stanford, California 94305

Author Email: horvitz@microsoft.com

Abstract:

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.

Keywords: Theorem proving, control of theorem proving, time-critical reasoning, Bayesian methods, decision making under bounded resources, decision-theoretic methods, Polya

In: Proceedings of Eleventh Conference on Uncertainty in Artificial Intelligence, Montreal, August 1995, pages 306-314. Morgan Kaufmann: San Francisco.