Abstract
Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and nontermination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing stateoftheart algorithms can only semidecide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it
does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing.
Recently, an algorithm was presented that semidecides a weaker property – of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper we strengthen these recent results. We propose a method that semidecides productivity of individual derivations for regular formulae. Thus we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.
does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing.
Recently, an algorithm was presented that semidecides a weaker property – of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper we strengthen these recent results. We propose a method that semidecides productivity of individual derivations for regular formulae. Thus we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.
Original language  English 

Pages (fromto)  906923 
Number of pages  18 
Journal  Theory and Practice of Logic Programming 
Volume  17 
Issue number  56 
Early online date  22 Aug 2017 
DOIs  
Publication status  Published  Sep 2017 
Event  33rd International Conference on Logic Programming  Melbourne, Australia Duration: 28 Aug 2017 → 1 Sep 2017 
Keywords
 Horn Clauses
 (Co)Recursion
 (Co)Induction
 Infinite term trees
 Productivity
Fingerprint Dive into the research topics of 'Productive Corecursion in Logic Programming'. Together they form a unique fingerprint.
Profiles

Ekaterina Komendantskaya
 School of Mathematical & Computer Sciences  Professor
 School of Mathematical & Computer Sciences, Computer Science  Professor
Person: Academic (Research & Teaching)