首页   按字顺浏览 期刊浏览 卷期浏览 Increasing the efficiency of automated theorem proving
Increasing the efficiency of automated theorem proving

 

作者: Gabriel Aguilera,   InmaP. de Guzmán,   Manuel Ojeda,  

 

期刊: Journal of Applied Non-Classical Logics  (Taylor Available online 1995)
卷期: Volume 5, issue 1  

页码: 9-29

 

ISSN:1166-3081

 

年代: 1995

 

DOI:10.1080/11663081.1995.10510841

 

出版商: Taylor & Francis Group

 

数据来源: Taylor

 

摘要:

In this work a new Automated Theorem Prover (ATP) via refutation for classical logic and which does not require the conversion to clausal form, named TAS-D++, is introduced. The main objective in the design of this ATP was to obtain a parallel and computationally efficient method naturally extensible to non-standard logics (concretely, to temporal logics, see [12]). TAS-D++works by using transformations of the syntactic trees of the formulas and, as tableaux and matrix style provers [6, 15, 16], it is Gentzen-based. Its power is mainly based in the efficient extraction of implicit information in the syntactic trees (in difference with the standard ATPs via refutation) to detect both:

 

点击下载:  PDF (785KB)



返 回