Appeal No. 2000-0168
Application No. 08/934,393
APPENDIX
Claim 27
27. A computer-implemented method of automated
proving for unrestricted first-order logic to test
the unsatisfiability of a set of input terms (Q)
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 (Q) onto an equivalent generalized term
defined as a triplet <Q,,,i>, where , is an empty
substitution and i is an empty set, to form a set
(E)of generalized terms;
(2) applying, in the computer, to the set
(E) an instance extraction rule (IE) defined as
follows:
(IE) E 6 (E -{Q<F,7>})c(Q<FF,7*FF>,Q<F,7c{FF}>)
where F is a substitution, 7 is a finite set of
standard substitutions {7 ,..., 7 }, the doublet <F,1 <
7> is a generalized substitution which maps a
standard term onto a generalized term defined as a
triplet <Q,F,7> such that <Q,F,7> = <Q,F,7>, F is a
substitution valid for the generalized term <Q,F,7>
and QF is an instance of Q yielded by the
substitution F and is a standard term equivalent to
the generalized term <Q,F,i> 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) Q<F,7>
Q<FF,7*FF>
9
Page: Previous 1 2 3 4 5 6 7 8 9 10 Next
Last modified: November 3, 2007