slide0060.htm

人工智能的教材啊

 "Times New Roman"'> </span><span style='font-family:Symbol;mso-char-type:symbol'><i>F</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span>和<span style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span style='font-family:Symbol;mso-char-type:symbol'><i>Y</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span>的基例<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'>, </span>若<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'><i> X’</i></span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>是<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'> </span><span style='font-family:
 Symbol;mso-char-type:symbol'><i>F</i></span><span style='font-family:"Times New Roman";
 mso-hansi-font-family:"Times New Roman"'><i>’</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span>和<span style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span style='font-family:Symbol;mso-char-type:symbol'><i>Y</i></span><span
 style='font-family:"Times New Roman";mso-hansi-font-family:"Times New Roman"'><i>’</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span>的归结结果<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'>, &#13;</span></div>
 <div style='position:absolute;top:36.5%;left:5.8%;width:103.18%;height:5.75%'>则存在一个<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span style='font-family:Symbol;mso-char-type:symbol'><i>F</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span>和<span style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span style='font-family:Symbol;mso-char-type:symbol'><i>Y</i></span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'><i>
 </i></span>的归结结果<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'> </span><span lang=EN-US style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman";mso-fareast-language:ZH-CN'><i>X</i></span><span
 lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'>, </span>使得<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'> </span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'><i>X’</i></span><span lang=EN-US style='font-family:
 "Times New Roman";mso-ascii-font-family:"Times New Roman";mso-fareast-language:
 ZH-CN'> </span>是<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'> </span><span lang=EN-US style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman";mso-fareast-language:ZH-CN'><i>X</i></span><span
 lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>得替换情形<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'>.&#13;</span></div>
 <div style='position:absolute;top:42.25%;left:5.8%;width:93.44%;height:5.25%'>证<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>:&#13;</span></div>
 <div style='position:absolute;top:48.0%;left:5.8%;width:93.44%;height:4.75%'>&#13;</div>
 <div style='position:absolute;top:52.75%;left:5.8%;width:105.61%;height:5.25%'><span
 style='font-family:黑体;mso-ascii-font-family:黑体;mso-fareast-font-family:黑体'>定理</span><span
 style='font-family:宋体;mso-ascii-font-family:宋体'>[提升定理]</span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'><i>
 </i></span><span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'><span style="mso-spacerun: yes">&nbsp;</span></span>若<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>S’ </i></span>是一个子句集<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>S</i></span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>的基例<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'>, </span>且存在一个从&#13;</div>
 <div style='position:absolute;top:58.25%;left:5.8%;width:105.43%;height:5.25%'><span
 lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'><i>S’</i></span><span lang=EN-US style='font-family:
 "Times New Roman";mso-ascii-font-family:"Times New Roman";mso-fareast-language:
 ZH-CN'> </span>到子句<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'> </span><span lang=EN-US style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman";mso-fareast-language:ZH-CN'><i>X </i></span>的归结演绎<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>,
 </span>则存在一个从<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'> </span><span lang=EN-US style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman";mso-fareast-language:ZH-CN'><i>S</i></span><span
 lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>到<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'> </span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'><i>X</i></span><span lang=EN-US style='font-family:
 "Times New Roman";mso-ascii-font-family:"Times New Roman";mso-fareast-language:
 ZH-CN'> </span>的归结演绎<span style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman"'>, </span>使&#13;</div>
 <div style='position:absolute;top:63.5%;left:5.8%;width:93.44%;height:5.25%'>得<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>X’ </i></span>是<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>X</i></span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>得替换情形<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'>.&#13;</span></div>
 <div style='position:absolute;top:68.75%;left:5.8%;width:93.44%;height:5.25%'>证<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>:<span
 style="mso-spacerun: yes">&nbsp; </span>&#13;</span></div>
 <div style='position:absolute;top:74.5%;left:5.8%;width:93.44%;height:4.75%'>&#13;</div>
 <div style='position:absolute;top:79.5%;left:5.8%;width:108.23%;height:5.25%'><span
 style='font-family:黑体;mso-ascii-font-family:黑体;mso-fareast-font-family:黑体'>定理</span><span
 style='font-family:宋体;mso-ascii-font-family:宋体'>[完全性定理]</span><span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'><i><span
 style="mso-spacerun: yes">&nbsp; </span></i></span>若一个子句集<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>S</i></span><span lang=EN-US
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman";
 mso-fareast-language:ZH-CN'> </span>是不可满足的<span style='font-family:"Times New Roman";
 mso-ascii-font-family:"Times New Roman"'>, </span>则存在一个&#13;</div>
 <div style='position:absolute;top:84.75%;left:5.8%;width:93.44%;height:5.25%'>从<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>
 </span><span lang=EN-US style='font-family:"Times New Roman";mso-ascii-font-family:
 "Times New Roman";mso-fareast-language:ZH-CN'><i>S </i></span>到空子句的归结演绎<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>.&#13;</span></div>
 <div style='position:absolute;top:90.0%;left:5.8%;width:93.44%;height:5.25%'>证<span
 style='font-family:"Times New Roman";mso-ascii-font-family:"Times New Roman"'>:<span
 style="mso-spacerun: yes">&nbsp; </span></span></div>
 </div>
</p:slide></div>

</body>

</html>