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.

In Proceedings CoALP-Ty'16, arXiv:1709.04199

References in corpus (2)

• Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
• Structural Resolution for Logic Programming

Cited by in corpus (1)

• Structural Resolution for Abstract Compilation of Object-Oriented Languages