Patent ID: 6424962
Filing Date: 2002-07-23
Classification: G06N

Abstract:
A computer-implemented method of automated proving for unrestricted first-order logic to test the unsatisfiability of a set of input terms (&PSgr;) representative of clauses or superclauses, the set of input terms describing an industrial system, the method comprising the steps of:(1) mapping in a computer each of the input terms (&PSgr;) onto an equivalent generalized term defined as a triplet , where &egr; is an empty substitution and Ã˜ is an empty set, to form a set (&Sgr;) of generalized terms; (2) applying, in the computer, to the set (&Sgr;) an instance extraction rule (IE) defined as follows: (IE)&Sgr;â†’(&Sgr;âˆ’{&PSgr;})âˆª{&PSgr;,&PSgr;) where &sgr; is a substitution, &Lgr; is a finite set of standard substitutions {&lgr;1, . . . , &lgr;v}, the doublet  is a generalized substitution which maps a standard term onto a generalized term defined as a triplet  such that =&PSgr;, &mgr; is a substitution valid for the generalized term &PSgr; and &PSgr;&sgr; is an instance of &PSgr; yielded by the substitution &sgr; and is a standard term equivalent to the generalized term , the instance extraction rule (IE) resulting from an instance generation rule (IG) and an instance subtraction rule (IS), the instance generation rule being defined as: (IG)&it;â€ƒ&it;Î¨<Ïƒ,Î›>Î¨<Ïƒ&it;â€ƒ&it;Î¼,Î›*Ïƒ&it;â€ƒ&it;Î¼>and the instance subtraction rule being defined as:(IS)&PSgr;â†’&PSgr;meaning that the triplet &PSgr; should be replaced with &PSgr;, the step (2) resulting in a current set (&Sgr;);(3) generating, in the computer, a ground instance GIG(&Sgr;) of the current set &Sgr;, the ground instance generation GIG being a ground substitution replacing every variable with a same fixed constant and defined by the rule: (GIG)&it;â€ƒ&it;Î¨Î¨grwhere &PSgr;gr is a ground instance of term &PSgr;, the ground instance &PSgr;gr being obtained by replacing every variable with a same fixed constant;(4) applying and repeating steps (2) and (3) in the computer until the ground instance GIG(&Sgr;) of the current set (&Sgr;) is unsatisfiable; (5) determining, in the computer, the unsatisfiability of the set of input terms when the ground instance GIG(&Sgr;) is unsatisfiable; and (6) controlling development of the industrial system using information on the unsatisfiability of the input terms.