The current extended fuzzy description logics lack reasoning algorithms with TBoxes. The problem of the satisfiability of the extended fuzzy description logic EFALC cut concepts w. r. t. TBoxes is proposed, and a reas...The current extended fuzzy description logics lack reasoning algorithms with TBoxes. The problem of the satisfiability of the extended fuzzy description logic EFALC cut concepts w. r. t. TBoxes is proposed, and a reasoning algorithm is given. This algorithm is designed in the style of tableau algorithms, which is usually used in classical description logics. The transformation rules and the process of this algorithm is described and optimized with three main techniques： recursive procedure call, branch cutting and introducing sets of mesne results. The optimized algorithm is proved sound, complete and with an EXPTime complexity, and the satisfiability problem is EXPTime-complete.展开更多
After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable ...After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.展开更多
Asymptotic energy expansion method is extended for polynomial potentials having rational powers. New types of recurrence relations are derived for the potentials of the form rig, mN are positive integers while coeffic...Asymptotic energy expansion method is extended for polynomial potentials having rational powers. New types of recurrence relations are derived for the potentials of the form rig, mN are positive integers while coefficients bk ∈ C. As in the case of even degree polynomial potentials with integer powers, all the integrals in the expansion can be evaluated analytically in terms of F functions. With the help of two examples, we demonstrate the usefulness of these expansions in getting analytic insight into the quantum systems having rational power polynomial potentials.展开更多
基金The National Natural Science Foundation of China(No60403016),the Weaponry Equipment Foundation of PLA Equip-ment Ministry (No51406020105JB8103)
文摘The current extended fuzzy description logics lack reasoning algorithms with TBoxes. The problem of the satisfiability of the extended fuzzy description logic EFALC cut concepts w. r. t. TBoxes is proposed, and a reasoning algorithm is given. This algorithm is designed in the style of tableau algorithms, which is usually used in classical description logics. The transformation rules and the process of this algorithm is described and optimized with three main techniques： recursive procedure call, branch cutting and introducing sets of mesne results. The optimized algorithm is proved sound, complete and with an EXPTime complexity, and the satisfiability problem is EXPTime-complete.
基金supported by the Funds of the Chinese Academy of Sciences for Key Topics in Innovation Engineering under Grant No.KJCX2-YW-S02
文摘After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.
文摘Asymptotic energy expansion method is extended for polynomial potentials having rational powers. New types of recurrence relations are derived for the potentials of the form rig, mN are positive integers while coefficients bk ∈ C. As in the case of even degree polynomial potentials with integer powers, all the integrals in the expansion can be evaluated analytically in terms of F functions. With the help of two examples, we demonstrate the usefulness of these expansions in getting analytic insight into the quantum systems having rational power polynomial potentials.
