This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tre...This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.展开更多
This paper ① introduces an automatically reasoning system for inferring linearand quadratic surface solids from incomplete three views. The method is based on human reason-ing. Initially, quadratic surface primitives...This paper ① introduces an automatically reasoning system for inferring linearand quadratic surface solids from incomplete three views. The method is based on human reason-ing. Initially, quadratic surface primitives are recognized and extracted according to possibilitycomputation. Then, the data relative only to quadratic surface primitives are removed from thegiven three views and polyhedrons are constructed based on the remaining data. The final solidis constructed by assembling all the generated quadratic surface primitives and the polyhedrons.The system has been implemented in C and OpenGL on Windows NT. The constructed solidcan be observed at any angle by rotating it using the keyboard. Many examples are tested andthe experimental results show that the system is very robust, and can accurately and effectivelyconstruct a suitable solid composed of linear and quadratic surfaces from incomplete three views.展开更多
文摘This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.
文摘This paper ① introduces an automatically reasoning system for inferring linearand quadratic surface solids from incomplete three views. The method is based on human reason-ing. Initially, quadratic surface primitives are recognized and extracted according to possibilitycomputation. Then, the data relative only to quadratic surface primitives are removed from thegiven three views and polyhedrons are constructed based on the remaining data. The final solidis constructed by assembling all the generated quadratic surface primitives and the polyhedrons.The system has been implemented in C and OpenGL on Windows NT. The constructed solidcan be observed at any angle by rotating it using the keyboard. Many examples are tested andthe experimental results show that the system is very robust, and can accurately and effectivelyconstruct a suitable solid composed of linear and quadratic surfaces from incomplete three views.
