| 摘要 |
A method of automated proving for unrestricted first-logic to test the satisfiability of clause sets describing an industrial system which applies the instance generation rulewhere &PSgr; is a term, sigma a substitution and &PSgr;sigma an instance of &PSgr; yielded by the substitution sigma, and is characterized in that, instance subtraction is defined as the substraction of the instance &PSgr;sigma from &PSgr; resulting in a generalized term which is a triplet <&PSgr;, sigma, LAMBD> where LAMBD is a finite set of standard substitutions {lambd1, . . . , lambdn} and defined bythe method further applies an instance subtraction combined with said instance generation rule to get an instance extraction rule defined bywhere SIGMA is a set of clauses and mu is a substitution valid for the generalized term &PSgr;<sigma, LAMBD>, whereby the set SIGMA can be proven unsatisfiable.
|
