Method of automated proving for unrestricted first-order logic

Abstract From the Canadian patent

The method of automated proving for unrestricted first-logic to test the satisfiability of clause sets describing an industrial system applies the instance generation rule (IG)~~ ~.sigma. where ~ is a term .sigma. a substitution and ~.sigma. an instance of ~ yielded by the substitution .sigma. and is characterized in that defining an instance subtraction as the subtraction of the instance ~.sigma. from ~ resulting in a generalized term which is a triplet <~ .sigma. ~> where ~ is a finite set of standard substitutions {.lambda.1 ... .lambda.n} and defined by GE(<~, .sigma. ~>) = GE (~.sigma.)~ - GE ({~.lambda.1 ... ~.lambda.n}) the method further applies an instance subtraction combined with …