以文本方式查看主题

-  中文XML论坛 - 专业的XML技术讨论区  (http://bbs.xml.org.cn/index.asp)
--  『 算法理论与分析 』  (http://bbs.xml.org.cn/list.asp?boardid=60)
----  请教一个算法问题  (http://bbs.xml.org.cn/dispbbs.asp?boardid=60&rootid=&id=32630)

--  作者：shiwei_81515
--  发布时间：5/18/2006 4:42:00 PM

--  请教一个算法问题
我想实现一个归结法的算法.
算法思想：
设F={F1，…，Fn}为给定的公理集，设G为要求证明的定理，
且F，G都为子句的形式，则自动归结证明的过程为：
（1） 将F中的一切公式变成子句的形式；
（2） ～G将变成子句形式，并加入F的字句构成的字句集
S={C1，C2，…，Cn}；
（3） 在出现一个矛盾(空子句)或无任何进展之前执行:
     （3.1）从S中挑选一对子句C1与C2，并找到一个最一般合一元s使得：
           当C1s=（L1 V P）s = L1s V Ps
              C2s=（～L2 V Q）s = ～L2s V Qs
            有 L1s = L2s成立
     （3.2）令C12 = Ps V Qs  作为 C1 与C2 的归结式
     （3.3）若C12 为空子句，即找到矛盾，G得证；
            若C12 为非空子句 ，将C12加入S。

哪位高人能给点提示或者给点资料也行,小弟现在没法下手了!

--  作者：heyhelloworld
--  发布时间：6/5/2006 11:33:00 PM

--  
是 不是离散数学啊
--  作者：Logician
--  发布时间：6/5/2006 11:46:00 PM

--  
Logic for Computer Science - Foundations of Automatic Theorem Proving

基于归结方法的自动推理（分卷压缩，共3部分）



这两本书你可以看看。
其它的资料可以google“Automatic Theorem Proving”或“机器定理证明”。

--  作者：toniee
--  发布时间：7/10/2006 3:00:00 PM

--  
真是好资料啊，高！
W 3 C h i n a ( since 2003 ) 旗 下 站 点
苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
 66.406ms