|
|
|
|
  这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-06 23:35 | 107 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-07 02:05 | 78 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-07 22:32 | 53 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-08 05:31 | 122 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-09 01:59 | 287 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-09 02:50 | 115 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-09 14:15 | 117 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-10 04:14 | 58 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-11 01:30 | 277 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-11 01:56 | 1,073 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - attonie [ 2006-03-12 16:29 | 178 byte(s)]
Re: 这里有人作逻辑框架或者逻辑编程的吗? - lingcore [ 2006-03-13 11:56 | 201 byte(s)]
|
|
|
|
[Original]
[Print]
[Top]
|
现在的逻辑框架如果使用proof search的办法,好像很多问题都无法实现,所以需要对逻辑框架的形式化进行修改
Type实际上可以对proof search的过程可以起一些指导的作用,但是在很多逻辑框架中都没有类似的内容
现在type的研究是放在操作语义上做的,如果放入一个合适的逻辑框架,可能会比较有用
|
|
|
[Original]
[Print]
[Top]
|
|
[Original]
[Print]
[Top]
|
|
如果给表示能力强的逻辑框架找一个通用的proof search办法,当然描述的框架改变之后,经典的proof search办法是不能够再用,所以就需要引入其他一些概念才能满足我们的要求,这个就是需要我们做的
|
|
|
[Original]
[Print]
[Top]
|
|
[Original]
[Print]
[Top]
|
1。严格地讲，LF是用于定义逻辑系统的，证明只能在逻辑系统内做，而不是在LF中
做；
2。高价逻辑系统中没有通用证明方法；
3。ALF等系统中，通常通过定义tactics增加证明能力。
|
|
|
[Original]
[Print]
[Top]
|
|
|
声明: 本页内容为中国Linux论坛的内容镜像，文章的版权以及其他所有的相关权利属于中国Linux论坛和相应文章的作者，如果转载，请注明文章来源及相关版权信息。