Structural Resolution with Co-inductive Loop Detection

Yue Li

A way to combine co-SLD style loop detection with structural resolution was found and is introduced in this work, to extend structural resolution with co-induction. In particular, we present the operational semantics, called co-inductive structural resolution, of this novel combination and prove its soundness with respect to the greatest complete Herbrand model.

In Ekaterina Komendantskaya and John Power: Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types (CoALP-Ty'16), Edinburgh, UK, 28-29 November 2016, Electronic Proceedings in Theoretical Computer Science 258, pp. 52–67.
Published: 13th September 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.258.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org