A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set f...A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set for a difference polynomial set in general form to the union of difference polynomial sets in triangular form. Based on the characteristic set method, a decision procedure for the first order theory over an algebraically closed field and a procedure to prove certain difference identities are proposed.展开更多
A new type of intelligent CAI system for chemistry is developed inthis paPer based on automated reaJsoning with chemistry knowledge. The systemhas shown its ability to solve chemistry problems, to assist students and ...A new type of intelligent CAI system for chemistry is developed inthis paPer based on automated reaJsoning with chemistry knowledge. The systemhas shown its ability to solve chemistry problems, to assist students and teachersin studies and instruction with the automated reasoning functions. Its open modeof the knowledge base and its unique style of the illterface between the system andhuman provide more opportunities for the users to acquire living knowledge throughactive participation. The automated reasoning based on basic chemistry knowledgealso opened a new approach to the information storage and management of the ICAIsystem for sciences.展开更多
Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is repre...Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is representationtransform, but since its ifltermediate computing procedure is a black box from theviewpoint of the original problem, this aPproach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solvingSAT by Wu's method, a general algorithm for solving polynomial equations. By es-tablishing the correspondellce between the primitive operation in Wu's method andclause resolution in SAT, it is shown that Wu's method, when used for solving SAT,is primarily a restricted clause resolution procedure. While Wu's method illtroduceselltirely new concepts, e.g. characteristic set of clauses, to resolution procedure, thecomplexity result of resolution procedure suggests an exponential lower bound toWu's method for solving general polynomial equations. Moreover, this algorithmtransform can help achieve a more efficiellt imp1ementation of Wu's method since itcan avoid the complex manipulation of polynomials and can make the best use ofdomain specific knowledge.展开更多
As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice impl...As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra.In this principle,the resolution level is an ideal of lattice implication algebra,instead of an element in truth-value field.Moreover,the soundness theorem is given.In the light of lifting lemma,the completeness theorem is established.This can provide a new tool for automated reasoning.展开更多
Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal au...Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal automated rea-soning systems, thus the efficiency of the whole system is improved. This paper presents some global properties of valid formulas in modal logic K. Such prop-erties are structure characters of formulas, so they are simple and easy to check.At the same time, some global properties of K unsatisfiable formula set are also given.展开更多
Extracting justifications for web ontology language(OWL)ontologies is an important mission in ontology engineering.In this paper,we focus on black-box techniques which are based on ontology reasoners.Through creating ...Extracting justifications for web ontology language(OWL)ontologies is an important mission in ontology engineering.In this paper,we focus on black-box techniques which are based on ontology reasoners.Through creating a recursive expansion procedure,all elements which are called critical axioms in the justification are explored one by one.In this detection procedure,an axiom selection function is used to avoid testing irrelevant axioms.In addition,an incremental reasoning procedure has been proposed in order to substitute series of standard reasoning tests w.r.t.satisfiability.It is implemented by employing a pseudo model to detect“obvious”satisfiability directly.The experimental results show that our proposed strategy for extracting justifications for OWL ontologies by adopting incremental expansion is superior to traditional Black-box methods in terms of efficiency and performance.展开更多
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.展开更多
基金This work is supported by the National Grand Fundamental Research 973 Program of China under Grant No. 2004CB318000. Acknowledgement We would like to take this opportunity to express our deep gratitude to the National Natural Science Foundation of China （NSFC） for its support during the past twenty years. Without the support from NSFC, mathematics mechanization is impossible to be so prosperous today. The second author would like, in particular, to thank NSFC for an 0utstanding Young Investigator Award for the period 1998 to 2001.
文摘A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set for a difference polynomial set in general form to the union of difference polynomial sets in triangular form. Based on the characteristic set method, a decision procedure for the first order theory over an algebraically closed field and a procedure to prove certain difference identities are proposed.
文摘A new type of intelligent CAI system for chemistry is developed inthis paPer based on automated reaJsoning with chemistry knowledge. The systemhas shown its ability to solve chemistry problems, to assist students and teachersin studies and instruction with the automated reasoning functions. Its open modeof the knowledge base and its unique style of the illterface between the system andhuman provide more opportunities for the users to acquire living knowledge throughactive participation. The automated reasoning based on basic chemistry knowledgealso opened a new approach to the information storage and management of the ICAIsystem for sciences.
文摘Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is representationtransform, but since its ifltermediate computing procedure is a black box from theviewpoint of the original problem, this aPproach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solvingSAT by Wu's method, a general algorithm for solving polynomial equations. By es-tablishing the correspondellce between the primitive operation in Wu's method andclause resolution in SAT, it is shown that Wu's method, when used for solving SAT,is primarily a restricted clause resolution procedure. While Wu's method illtroduceselltirely new concepts, e.g. characteristic set of clauses, to resolution procedure, thecomplexity result of resolution procedure suggests an exponential lower bound toWu's method for solving general polynomial equations. Moreover, this algorithmtransform can help achieve a more efficiellt imp1ementation of Wu's method since itcan avoid the complex manipulation of polynomials and can make the best use ofdomain specific knowledge.
基金the National Natural Science Foundation of China(No.61175055)the Sichuan Key Technology Research and Development Program(No.2011FZ0051)
文摘As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra.In this principle,the resolution level is an ideal of lattice implication algebra,instead of an element in truth-value field.Moreover,the soundness theorem is given.In the light of lifting lemma,the completeness theorem is established.This can provide a new tool for automated reasoning.
文摘Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal automated rea-soning systems, thus the efficiency of the whole system is improved. This paper presents some global properties of valid formulas in modal logic K. Such prop-erties are structure characters of formulas, so they are simple and easy to check.At the same time, some global properties of K unsatisfiable formula set are also given.
基金Research presented in this paper was partially supported by the National Natural Science Foundation of China(Grant Nos.61672261,61502199)It’s also funded by China Scholarship Council(201506175028)for the first author of this paper.
文摘Extracting justifications for web ontology language(OWL)ontologies is an important mission in ontology engineering.In this paper,we focus on black-box techniques which are based on ontology reasoners.Through creating a recursive expansion procedure,all elements which are called critical axioms in the justification are explored one by one.In this detection procedure,an axiom selection function is used to avoid testing irrelevant axioms.In addition,an incremental reasoning procedure has been proposed in order to substitute series of standard reasoning tests w.r.t.satisfiability.It is implemented by employing a pseudo model to detect“obvious”satisfiability directly.The experimental results show that our proposed strategy for extracting justifications for OWL ontologies by adopting incremental expansion is superior to traditional Black-box methods in terms of efficiency and performance.
基金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.
