金色年华(教学参考)
金色年華(教學參攷)
금색년화(교학삼고)
GOLDEN TIMES
2011年
6期
89-90
,共2页
归结原理%人工智能%机器证明%水平浸透法
歸結原理%人工智能%機器證明%水平浸透法
귀결원리%인공지능%궤기증명%수평침투법
归结原理使用较广,是定理机器证明的理论基础.既可以用来证明一些目标公式和逻辑结论的成立,又可以用来求解应用问题的答案.比如一个目标公式xW(x),有时我们不但要求证明它成立,而且希望知道变元x的一个例,即如果回答x=A,W是否为真?可直接用归结反演证明,但要回答x=?W为真时,就需要问题的答案.本文给出了归结原理在这两方面的应用,最后指出了使用水平浸透法证明不可满足性所带来的子句冗余,以及避免子句冗余的一个方法.
歸結原理使用較廣,是定理機器證明的理論基礎.既可以用來證明一些目標公式和邏輯結論的成立,又可以用來求解應用問題的答案.比如一箇目標公式xW(x),有時我們不但要求證明它成立,而且希望知道變元x的一箇例,即如果迴答x=A,W是否為真?可直接用歸結反縯證明,但要迴答x=?W為真時,就需要問題的答案.本文給齣瞭歸結原理在這兩方麵的應用,最後指齣瞭使用水平浸透法證明不可滿足性所帶來的子句冗餘,以及避免子句冗餘的一箇方法.
귀결원리사용교엄,시정리궤기증명적이론기출.기가이용래증명일사목표공식화라집결론적성립,우가이용래구해응용문제적답안.비여일개목표공식xW(x),유시아문불단요구증명타성립,이차희망지도변원x적일개례,즉여과회답x=A,W시부위진?가직접용귀결반연증명,단요회답x=?W위진시,취수요문제적답안.본문급출료귀결원리재저량방면적응용,최후지출료사용수평침투법증명불가만족성소대래적자구용여,이급피면자구용여적일개방법.
