7 citations · 13 across the 5 of their papers we have counts for
5 papers
Coinductive Uniform Proofs
Ekaterina Komendantskaya, Yue Li
Coinduction occurs in two guises in Horn clause logic: in proofs of circular properties and relations, and in proofs involving construction of infinite data. Both instances of coin…
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
Henning Basold, Ekaterina Komendantskaya, Yue Li
We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolu…
Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
Ekaterina Komendantskaya Dr, Yue Li
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite…
Productive Corecursion in Logic Programming
Ekaterina Komendantskaya, Yue Li
Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soun…
Structural Resolution with Co-inductive Loop Detection
Yue Li
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,…