METHOD OF AUTOMATED PROVING FOR UNRESTRICTED FIRST-ORDER LOGIC

摘要

The method of automated proving for unrestrictedfirst-logic to test the satisfiability of clause sets describingan 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 theinstance ~.sigma. from ~ resulting in a generalized term which isa triplet ~, .sigma., ~ where ~ is a finite set of standardsubstitutions {.lambda.1, ..., .lambda.n} and defined byGE(~, .sigma., ~) = GE (~.sigma.)~ - GE ({~.lambda.1, ..., ~.lambda.n})the method further applies an instance subtraction combinedwith said instance generation rule to get an instanceextraction rule defined by(IE) .SIGMA. ~ (.SIGMA. - {~.sigma.,~})~{~.sigma.µ, ~*.sigma.µ,~.sigma., ~~{.sigma.µ})where .SIGMA. is a set of clauses and µ is a substitution validfor the generalized term ~.sigma., ~, whereby the set .SIGMA. can beproved unsatisfiable.