SLD-resolution without occur-check, an example

Autor:	Drabent, Włodzimierz
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science Computer Science - Programming Languages 68N17 03B10 D.1.6 F.3.3
Druh dokumentu:	Working Paper
Popis:	We prove that the occur-check is not needed for a certain definite clause logic program, independently from the selection rule. First we prove that the program is occur-check free. Then we consider a more general class of queries, under which the program is not occur-check free; however we show that it will be correctly executed under Prolog without occur-check. The main result of this report states that the occur-check may be skipped for the cases in which a single run of a standard nondeterministic unification algorithm does not fail due to the occur-check. The usual approaches are based on the notion of NSTO (not subject to occur-check), which considers all the runs. To formulate the result, it was necessary to introduce an abstraction of a "unification" algorithm without the occur-check. Comment: 9 pages. This version: small corrections, mainly p.7
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2103.01911 Zobrazit plný text záznamu View this record from Arxiv