命题逻辑的自动化解析
命题逻辑的自动化解析

作者:boater 提交日期:2006-10-10 20:01:00

恐怖主义是邪恶的。---9.11


有时候会撞到纯逻辑的推理题,如果能用机器求解的话,事情就会变得相对容易些。人脑必竟是肉做的,跑得过机器吗?
有些推理题是可以自动化解析的。偶(部分地)实现了这个梦想。
1.对命题公式最为机械的解析方式是生成其真值表,以遍历各变元所有可能的结果取值之组合,以及该组合情形下的命题公式的真假。但这可能会造成大量运算,故采用它法。
2.我个人习惯于通过在纸面上画出逻辑树来最终生成各分支均为真的树来。操作中发现:逻辑树产生了大量的分支,若以有向图的形式来表示逻辑分支更为可取。
3.在图中,每一个命题(复合命题,简单命题或命题变元)用一个结点表示
初始状态时,解析代表整个命题公式的结点n。设n=a->^b.当发现其不是变元(有待进一步解析)时,
  将其扩展为平行式:
    a---^b
   ^a--- b
   ^a---^b
  平行式右侧之子系其左侧之变元。左侧ni之子系ni.son.
  然后,以递归方式(以上所述)依次解析平行式右侧之命题。
4.第3步说明了递归解析的方式,在解析中需注意以下几点:
  a.对图结点的遍历与对图中路径的遍历是不同的概念。
  b.一个结点可能系多条路径的交叉点。
  c.若当前结点系变元时,需立即判断在当前逻辑分支中加入此变元后,逻辑上是否归谬(通过全局变量path来判断)。若归谬,需在结点中记录使其归谬时的路径信息(万不可将其删除之)。
  d.当结点无子可遍历或结点归谬时,回退一步。(path.pop()),否则path.push(n);当结点无父时,将其加入root.
5.解析的最终结果是一个图结构。root中存放着图中若干个遍历的起始结点。依次对其中的结点深度优先遍历(遍历时需抛弃已归谬的路径),遍历所得的每一条路径系一个可行的解(即:析取范式中的一个合取项).


(尚未实现对谓词逻辑的解析。)


========================
问题就这样解决了,我们可轻易地加入一点代码,使其实现相关功能。


以下推理题及其解答均系程序自动生成:
a,b,c,d,f,g,h,i,j,k,l,m,n,p,q,r,t 17 个人想进行围棋赛,关于谁参加比赛,下列几个判断是正确的:
1:要么m和r都参加,要么m和r都不参加,
2:要么c参加h不参加,要么c不参加,h参加,
3:不可能q不参加且d参加,
4:要么j和i都参加,要么j和i都不参加,
5:q和r至少有一个不参加,
6:要么d和f都参加,要么d和f都不参加,
7:若t参加,则m必定参加,
8:不可能n不参加且d参加,
9:要么c和f都参加,要么c和f都不参加,
10:若i不参加,则a必定也不参加,
11:要么k参加b不参加,要么k不参加,b参加,
12:不可能j不参加且i参加,
13:要么l参加h不参加,要么l不参加,h参加,
14:要么p参加j不参加,要么p不参加,j参加,
15:不可能g参加且i不参加,
16:要么a参加j不参加,要么a不参加,j参加,
17:不可能n参加且j不参加,
18:g参加,h不参加,
19:要么q,f都参加,要么q,f都不参加,
20:不可能a参加且p不参加,
21:a,b,c,d中至少有一个不参加,
请找出谁参加了比赛。


答案是:
参加者:d,c,g,l,b,q,i,f,j,n;不参加者:t,p,m,h,r,a,k


哼哼,有点意思...


 

#日志日期:2006-9-11 星期一(Monday) 晴 送小红花 推荐指数:复制链接 举报
天涯“2016年度十大最具影响力博客”评选


登录 | 新人注册>>
输入您的评论:(不支持HTML标签)


验证码
本文所属博客:IT,软件
引用地址:
© 天涯社区