Loop elimination, a sound optimisation technique for PTTP related theorem proving

Zombori Zsolt and Szeredi Péter: Loop elimination, a sound optimisation technique for PTTP related theorem proving. In: Acta cybernetica, (20) 3. pp. 441-458. (2012)

[thumbnail of actacyb_20_3_2012_5.pdf]
Preview
Cikk, tanulmány, mű
actacyb_20_3_2012_5.pdf

Download (138kB) | Preview

Abstract

In this paper we present loop elimination, an important optimisation technique for first-order theorem proving based on Prolog technology, such as the Prolog Technology Theorem Prover or the DLog Description Logic Reasoner. Although several loop checking techniques exist for logic programs, to the best of our knowledge, we are the first to examine the interaction of loop checking with ancestor resolution. Our main contribution is a rigorous proof of the soundness of loop elimination.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2012
Volume: 20
Number: 3
ISSN: 0324-721X
Page Range: pp. 441-458
Language: English
Place of Publication: Szeged
Related URLs: http://acta.bibl.u-szeged.hu/38533/
DOI: 10.14232/actacyb.20.3.2012.5
Uncontrolled Keywords: Számítástechnika, Kibernetika
Additional Information: Bibliogr.: p. 456-458. ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2016. Oct. 17. 10:38
Last Modified: 2022. Jun. 17. 14:51
URI: http://acta.bibl.u-szeged.hu/id/eprint/30840

Actions (login required)

View Item View Item