Loop elimination, a sound optimisation technique for PTTP related theorem proving
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 b...
Elmentve itt :
| Szerzők: | |
|---|---|
| Dokumentumtípus: | Cikk |
| Megjelent: |
2012
|
| Sorozat: | Acta cybernetica
20 No. 3 |
| Kulcsszavak: | Számítástechnika, Kibernetika |
| Tárgyszavak: | |
| doi: | 10.14232/actacyb.20.3.2012.5 |
| Online Access: | http://acta.bibl.u-szeged.hu/30840 |
| LEADER | 01330nab a2200241 i 4500 | ||
|---|---|---|---|
| 001 | acta30840 | ||
| 005 | 20220617145150.0 | ||
| 008 | 161017s2012 hu o 0|| eng d | ||
| 022 | |a 0324-721X | ||
| 024 | 7 | |a 10.14232/actacyb.20.3.2012.5 |2 doi | |
| 040 | |a SZTE Egyetemi Kiadványok Repozitórium |b hun | ||
| 041 | |a eng | ||
| 100 | 1 | |a Zombori Zsolt | |
| 245 | 1 | 0 | |a Loop elimination, a sound optimisation technique for PTTP related theorem proving |h [elektronikus dokumentum] / |c Zombori Zsolt |
| 260 | |c 2012 | ||
| 300 | |a 441-458 | ||
| 490 | 0 | |a Acta cybernetica |v 20 No. 3 | |
| 520 | 3 | |a 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. | |
| 650 | 4 | |a Természettudományok | |
| 650 | 4 | |a Számítás- és információtudomány | |
| 695 | |a Számítástechnika, Kibernetika | ||
| 700 | 0 | 1 | |a Szeredi Péter |e aut |
| 856 | 4 | 0 | |u http://acta.bibl.u-szeged.hu/30840/1/actacyb_20_3_2012_5.pdf |z Dokumentum-elérés |