| Decision Making as Theorem Proving |
| |
| 作者姓名： | Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering P.O. Box - Beijing P.R.China |
| |
| 作者单位： | Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering，P.O. Box 9702-19，Beijing 100101，P.R.China |
| |
| 摘 要： | 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.
|
Decision Making as Theorem Proving |
| |
| Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering,P.O. Box -,Beijing ,P.R.China.Decision Making as Theorem Proving[J].Journal of Systems Engineering and Electronics,1993(1). |
| |
| Authors: | Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering PO Box - Beijing PRChina |
| |
| Institution: | Zhu Mingyuan and Wang ChengweiBeijing Institute of Systems Engineering,P.O. Box 9702-19,Beijing 100101,P.R.China |
| |
| Abstract: | 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. |
| |
| Keywords: | Decision support system Theorem proving Type theory |
| 本文献已被 CNKI 等数据库收录！ |
