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

Zombori Zsolt; 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]
Előnézet
Cikk, tanulmány, mű
actacyb_20_3_2012_5.pdf

Letöltés (138kB) | Előnézet

Absztrakt (kivonat)

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.

Mű típusa: Cikk, tanulmány, mű
Befoglaló folyóirat/kiadvány címe: Acta cybernetica
Dátum: 2012
Kötet: 20
Szám: 3
ISSN: 0324-721X
Oldalak: pp. 441-458
Nyelv: angol
Kiadás helye: Szeged
Befoglaló mű URL: http://acta.bibl.u-szeged.hu/38533/
DOI: 10.14232/actacyb.20.3.2012.5
Kulcsszavak: Számítástechnika, Kibernetika
Megjegyzések: Bibliogr.: p. 456-458. ; összefoglalás angol nyelven
Szakterület: 01. Természettudományok
01. Természettudományok > 01.02. Számítás- és információtudomány
Feltöltés dátuma: 2016. okt. 17. 10:38
Utolsó módosítás: 2022. jún. 17. 14:51
URI: http://acta.bibl.u-szeged.hu/id/eprint/30840
Bővebben:
Tétel nézet Tétel nézet