Appeal No. 2000-0168
Application No. 08/934,393
and the instance subtraction rule being defined as:
(IS) Q <F,7> 6 Q <F,7c{FF}>
meaning that the triplet Q <F, 7> should be replaced
with Q <F,7c{FF}>, the step (2) resulting in a
current set (E);
(3) generating, in the computer, a ground
instance GIG(E) of the current set E, the ground
instance generation GIG being a ground substitution
replacing every variable with a same fixed constant
and defined by the rule:
(GIG) Q
Qgr
where Q is a ground instance of term Q, the ground
gr
instance Q being obtained by replacing every
gr
variable with a same fixed constant;
(4) applying and repeating steps (2) and (3) in
the computer until the ground instance GIG(E) of the
current set (E) is unsatisfiable;
(5) determining, in the computer, the
unsatisfiability of the set of input terms when the
ground instance GIG(E) is unsatisfiable; and
(6) controlling development of the
industrial system using information on the
unsatisfiability of the input terms.
10
Page: Previous 1 2 3 4 5 6 7 8 9 10
Last modified: November 3, 2007