| « | may 2026 | » | | 日 | 一 | 二 | 三 | 四 | 五 | 六 | | | | | | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | 24 | 25 | 26 | 27 | 28 | 29 | 30 | 31 | | | | | | | |
|
公告 |
| 暂无公告... |
| Blog信息 |
|
blog名称:
日志总数:3
评论数量:4
留言数量:0
访问次数:41411
建立时间:2005年11月18日 |
| |
|
 关于ASP的一些小性质和其证明。
文章收藏
cairc 发表于 2005/12/25 12:50:02 |
| 转载自: http://ai.ustc.edu.cn/sharepoint/tiki-view_blog.php?blogId=76关于ASP的一些小性质和其证明。 说明： （1）一个ASP程序P，又两部分构成，R为规则集，包括default规则和一些命题形式（非 default）规则，统一的形式为，L0 <- L1, L2,..., Lk, not Lk+1,..., not Ln。F为事实集，表 达当前事实（context），形式为，L <- 。 （2）对于一个规则集R，其中所有出现在not后的文字构成的集合，记为NL。 （3）对于一个规则集R，一个文字集X，定义R*X表示根据X删除R中规则和not后得到正程序。 （4）AS(R,F)，表示又R并F构成的ASP程序的AS集。对于正程序，就表示其AS。 （5）p，p1，p2表示文字集，也可对应为事实。 Lemma 1 : 对于某个R，任意X，X包含于NL，如果 AS(R*X, X)和NL的交集包含于X，则必然存在事实集F，使得 ，对于ASP程序的某个AS A，有R*X= R*A。 证：取F'=AS(R*X, X)，则满足后面的要求，得证。+ Lemma 2 : 对于某个R，任意F，有ASP程序，对的任意AS A，必然存在X，X包含于NL，使得AS(R*X, X)和NL的交集包含于X，且R*X=R*A。 证：取X'为A和NL的交集，则满足要求，得证。+ Lemma 3: 对某个R，任意X，X包含于NL，如果 AS(R*X, X\/p)和NL的交集包含于X，则必然存在事实集F，使得，对于ASP程序的某个AS A，有R*X= R*A，且p包含与A。 证：取F=AS(R*X, p\/X)，则满足要求，得证。+ Lemma 4: 对于某个R，任意F，有ASP程序，对的任意AS A，p包含于A，则必然存在X，X包含于NL，使得AS(R*X, X\/p)和NL的交集包含于X，且R*X=R*A。 Def : p1 |-(R) p2定义为：对任意X，若X包含于NL，且AS(R*X, X\/p1)和NL的交集包含于X，则必要p2包含于AS(R*X, p1\/X)。 Them : p1 |-(R) p2 iff 对任意F，对于ASP程序，对的任意AS A，若p1包含于A则必有p2包含于A。 证：懒得打了。用到了Lemma 3和Lemma 4。+ 总结：1。前面引理发现了对于一个R可能的reduction或信念扩展的方式需满足的条件。 2。在特定知识p下reduction或信念扩展的方式需满足的条件。 3。定义了两文字集间关于某个R上的推出关系，以此可以有很多应用，一个就是特殊优先。 下一步工作： 1。扩展p1 |-(R) p2，定义类似的两规则体间的推出关系，即加入not的处理。 2。沿着利用特殊优先结局矛盾或AS间排序这条路，利用前面定义的p1 |-(R) p2，将其补全成为一个完整的东西。 3。考虑其他应用。 4。ASP是混在一块的，Default logic在命题逻辑下形式，从知识表达的角度，考虑ASP程序中规则应如何分类，并表达对应的知识。 5。考虑，Reiter的normal default theory中规则特殊形式，在ASP中类似考虑。 |
|
|