從歸結(jié)證明樹(shù)抽取程序.pdf

1、對(duì)于形如( x)( y)P(x,y)的定理證明問(wèn)題,利用歸結(jié)原理可以回答其是否為真,而對(duì)于"對(duì)每個(gè)確定的x,y的值是什么?"這一經(jīng)典的證明論問(wèn)題,歸結(jié)原理則無(wú)能為力.有許多人研究從歸結(jié)證明樹(shù)確定y的值的方法.比較有代表性的是Green的方法和Luckham的方法.但由于他們的方法都不是從分析歸結(jié)證明過(guò)程出發(fā)的,所以他們的方法存在許多局限性.在這篇論文中,我們主要做了如下兩項(xiàng)工作:第一,對(duì)于形如( x)( y)P(x,y)的定理證明問(wèn)題,

2、該文從分析歸結(jié)證明樹(shù)中的每個(gè)節(jié)點(diǎn)入手,提取歸結(jié)證明的過(guò)程信息,生成一個(gè)程序.并且證明了抽取出的程序一定是部分正確的.這一方法的特點(diǎn)是,抽取算法的時(shí)間、空間復(fù)雜度都是線性的,并且抽取算法本身十分簡(jiǎn)單,易于實(shí)現(xiàn).第二,對(duì)于形如( x)( y)( z)P(x,y,z)的定理證明問(wèn)題,歸結(jié)證明樹(shù)中一定包含Skolem函數(shù),而由這樣的定理證明樹(shù)中抽取出的程序就有可能包含Skolem函數(shù).該文給出了是否能抽取出無(wú)Skolem函數(shù)的程序的充分必要條件