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: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: