# Structural Resolution with Co-inductive Loop Detection

## TL;DR

This paper introduces co-inductive structural resolution, combining co-SLD loop detection with structural resolution, and proves its soundness within logic programming semantics.

## Contribution

It presents the operational semantics of co-inductive structural resolution, extending structural resolution with co-induction, and establishes its soundness.

## Key findings

- Operational semantics for co-inductive structural resolution
- Proof of soundness with respect to the greatest Herbrand model
- Extension of structural resolution with co-inductive capabilities

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