Structural Resolution with Co-inductive Loop Detection
Logic in Computer Science
2017-09-15 v4
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.
Cite
@article{arxiv.1703.08336,
title = {Structural Resolution with Co-inductive Loop Detection},
author = {Yue Li},
journal= {arXiv preprint arXiv:1703.08336},
year = {2017}
}
Comments
In Proceedings CoALP-Ty'16, arXiv:1709.04199