Structural resolution with co-inductive loop detection

Yue Li

doi:10.4204/EPTCS.258.4

Structural resolution with co-inductive loop detection

Yue Li^*

^*Corresponding author for this work

School of Mathematical & Computer Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

42 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 language	English
Title of host publication	Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types
Publisher	Open Publishing Association
Pages	52-67
Number of pages	16
DOIs	https://doi.org/10.4204/EPTCS.258.4
Publication status	Published - 14 Sept 2017

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
Volume	258
ISSN (Print)	2075-2180

ASJC Scopus subject areas

Software

Access to Document

10.4204/EPTCS.258.4Licence: CC BY-SA

Download pdfFinal published version, 194 KBLicence: CC BY-SA

http://eptcs.web.cse.unsw.edu.au/paper.cgi?LPTI2016.4Licence: CC BY-SA

Cite this

@inproceedings{89d25bc02202435ea29e839494167625,

title = "Structural resolution with co-inductive loop detection",

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.",

author = "Yue Li",

year = "2017",

month = sep,

day = "14",

doi = "10.4204/EPTCS.258.4",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "52--67",

booktitle = "Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types",

address = "Australia",

}

TY - GEN

T1 - Structural resolution with co-inductive loop detection

AU - Li, Yue

PY - 2017/9/14

Y1 - 2017/9/14

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85030173712&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.258.4

DO - 10.4204/EPTCS.258.4

M3 - Conference contribution

AN - SCOPUS:85030173712

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 52

EP - 67

BT - Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types

PB - Open Publishing Association

ER -

Structural resolution with co-inductive loop detection

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this