Automated Reasoning and Equation Solving with the Characteristic Set Method

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.

The Intelligent CAI System for Chemistry Based on Automated Reasoning

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.

Solving SAT by Algorithm Transform of Wu's Method

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.

Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra

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.

The Global Properties of Valid Formulas in Modal Logic K

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 a justification for OWL ontologies by critical axioms

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.