Decision Making as Theorem Proving
Жу, Mingyuan, Wang, Chengwei · Acta Scientiarum Naturalium Universitatis Sunyatseni · 1993
We present a method for using type theory to solve decision making problem. Our method is based on the view that decision making is a special kind of theorem proving activity. An isomorphism between problems and types, and solutions and programs has been established to support this view which is much similar to the Curry-Howard isomorphism between propositions and types, and proofs and programs. To support our method, a proof development system called PowerEpsilon has been developed, and the synthesis of a decision procedure for validity of first-order prepositional logic is discussed to show the power of the system.