Patent US 6,424,962

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 rule where &PSgr; is a term, &sgr; a substitution and &PSgr;&sgr; an instance of &PSgr; yielded by the substitution &sgr;, and is characterized in that, instance subtraction is defined as the substraction of the instance &PSgr;&sgr; from &PSgr; resulting in a generalized term which is a triplet <&PSgr;, &sgr;, &Lgr;> where &Lgr; is a finite set of standard substitutions {&lgr;1, . . . , &lgr;n} and defined byGE(<&PSgr;, &sgr;, &Lgr;>)=GE(&PSgr;&sgr;)&#8722;GE({&PSgr;&lgr;1, . . . , &PSgr;&lgr;n})the method further applies an instance subtraction combined with said instance generation rule to get an instance extraction rule defined by(IE)&Sgr;&#8594;(&Sgr;&#8722;{&PSgr;<&sgr;,&Lgr;>})&#8746;{&PSgr;<&sgr;&mgr;,&Lgr;*&sgr;&mgr;>, &PSgr;<&sgr;,&Lgr;&#8746;{&sgr;&mgr;}>)where &Sgr; is a set of clauses and &mgr; is a substitution valid for the generalized term &PSgr;<&sgr;, &Lgr;>, whereby the set &Sgr; can be proven unsatisfiable.