Structural resolution with co-inductive loop detection

Yue Li

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types
PublisherOpen Publishing Association
Pages52-67
Number of pages16
DOIs
Publication statusPublished - 14 Sep 2017

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume258
ISSN (Print)2075-2180

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Structural resolution with co-inductive loop detection'. Together they form a unique fingerprint.

  • Cite this

    Li, Y. (2017). Structural resolution with co-inductive loop detection. In Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types (pp. 52-67). (Electronic Proceedings in Theoretical Computer Science; Vol. 258). Open Publishing Association. https://doi.org/10.4204/EPTCS.258.4