新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚
   XML论坛     W3CHINA.ORG讨论区     >>计算机科学论坛<<     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
    		•   Add to Google

    >> 本版讨论Semantic Web(语义Web,语义网或语义万维网, Web 3.0)及相关理论，如：Ontology(本体,本体论), OWL(Web Ontology Langauge,Web本体语言), Description Logic(DL, 描述逻辑),RDFa,Ontology Engineering等。
    [返回] 计算机科学论坛 → W3CHINA.ORG讨论区 - Web新技术讨论 → 『 Semantic Web(语义Web)/描述逻辑/本体 』 → 发个有趣的自动证明系统 ◇查看新帖 ◇ 用户列表 ◇

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 2823 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子　浏览下一篇主题
     * 贴子主题： 发个有趣的自动证明系统 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     wanggou 帅哥哟，离线，有人找我吗？
      
      
      威望：1
      等级：计算机学士学位(版主)
      文章：229
      积分：2047
      门派：XML.ORG.CN
      注册：2005/10/20

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给wanggou发送一个短消息 把wanggou加入好友 查看wanggou的个人资料 搜索wanggou在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 引用回复这个贴子 回复这个贴子 查看wanggou的博客楼主
    发贴心情 发个有趣的自动证明系统

    http://www.umsu.de/logik/trees/
    这里任给一个一阶逻辑的公式，它可以自动生成一个
    tree proof，速度很快，而且很好玩

       收藏   分享  
    顶(0)
      




    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/4 10:25:00
     
     wolfel 帅哥哟，离线，有人找我吗？
      
      
      威望：2
      等级：计算机学士学位
      文章：280
      积分：2178
      门派：W3CHINA.ORG
      注册：2005/3/17

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给wolfel发送一个短消息 把wolfel加入好友 查看wolfel的个人资料 搜索wolfel在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 引用回复这个贴子 回复这个贴子 查看wolfel的博客第2楼
    发贴心情 
    有意思，下面这段摘自它的help/background:

    What is a Tree Proof?
    The method of Tree Proofs, also known as Semantic Tableaux, is an effective algorithm for checking the validity of formulas in various logics. This website generates tableaux for classical propositional and predicate logic.

    How does it work?
    Internally, the script searches for a so-called free-variable tableau, which is then translated back into a familiar (sentence) tableau. The search uses backtracking with iterated deepening of the search space. At the same time, a simple countermodel detector tries to find a countermodel for the formula.

    是semantic tableau,跟DL的证明论是类似的，只是它针对一阶逻辑（的某个子集...）

    ----------------------------------------------
    Correct reasoning is our business.

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/4 19:43:00
     
     wanggou 帅哥哟，离线，有人找我吗？
      
      
      威望：1
      等级：计算机学士学位(版主)
      文章：229
      积分：2047
      门派：XML.ORG.CN
      注册：2005/10/20

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给wanggou发送一个短消息 把wanggou加入好友 查看wanggou的个人资料 搜索wanggou在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 引用回复这个贴子 回复这个贴子 查看wanggou的博客第3楼
    发贴心情 
    是啊，和DL的算法类似
    其实这类算法都是以语义树的构造为基础的
    感觉比机械证明的算法有效一些
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/5 8:49:00
     
     zhaonix 帅哥哟，离线，有人找我吗？
      
      
      威望：2
      头衔：博士
      等级：研一(日夜苦读RDF Semantics)
      文章：242
      积分：3185
      门派：W3CHINA.ORG
      注册：2005/4/18

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给zhaonix发送一个短消息 把zhaonix加入好友 查看zhaonix的个人资料 搜索zhaonix在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 点击这里发送电邮给zhaonix 引用回复这个贴子 回复这个贴子 查看zhaonix的博客第4楼
    发贴心情 
    有趣！Tableaux算法可以回到FOL中使用？！如果可判定的范围足够大的话，可就牛了X了，——要知道在以前不是没有FOL定理自动证明系统，但大多是基于归结（resolution）原理的。  试了一下，对第3个例子的证明中有一点与DL中的作法似乎不太一样：

    该命题是 \exists y \forall x(Fy \to Fx) 。其中从节点1到节点2和6，是对同一个\exists算符连续应用了两次 \exists-rule，分别引入变量a、b。 问题是：在第二次应用时，系统中已经存在了一个变量a对应于那个唯一的\exists算符，按照DL Tableau算法中的\exists-rule应用条件——见DL Handbook P85——，这时是不能对同一个算符再度应用同一\exists-rule的啊。
         是错了，还是Tableau算法在FOL下做了什么推广？困惑ing

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/5 21:31:00
     
     wolfel 帅哥哟，离线，有人找我吗？
      
      
      威望：2
      等级：计算机学士学位
      文章：280
      积分：2178
      门派：W3CHINA.ORG
      注册：2005/3/17

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给wolfel发送一个短消息 把wolfel加入好友 查看wolfel的个人资料 搜索wolfel在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 引用回复这个贴子 回复这个贴子 查看wolfel的博客第5楼
    发贴心情 
    这类tableau应该不能用于完全的FOL，而仍然是FOL的某个子集，因为FOL是不可判定的。tableau算法本来就跟自然演绎系统很类似，命题逻辑上也有tableau，可能还有别的。

    你提的第二个问题应该跟DL的tableau没关系，而是FOL上的那一套tableau的规则

    ----------------------------------------------
    Correct reasoning is our business.

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/5 22:19:00
     
     baojie 帅哥哟，离线，有人找我吗？
      
      
      
      威望：9
      头衔：小学生
      等级：研一(参加了一年一度的XML大会)(贵宾)
      文章：667
      积分：4442
      门派：XML.ORG.CN
      注册：2003/11/24

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给baojie发送一个短消息 把baojie加入好友 查看baojie的个人资料 搜索baojie在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 点击这里发送电邮给baojie  访问baojie的主页 引用回复这个贴子 回复这个贴子 查看baojie的博客第6楼
    发贴心情 
    这个tableau算法当然可以用在FOL上，只是不是完备（Complete）算法

    Tableau算法是一大类，FOL，模态逻辑等等都有。

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/11/6 1:30:00
     
     GoogleAdSense
      
      
      等级：大一新生
      文章：1
      积分：50
      门派：无门无派
      院校：未填写
      注册：2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 Semantic Web(语义Web)/描述逻辑/本体 』的所有贴子 点击这里发送电邮给Google AdSense  访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2025/10/6 6:05:18

    本主题贴数6，分页： [1]

    管理选项： 修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    		 78.125ms