Properties of Input-Consuming Derivations
Annalisa Bossi, Sandro Etalle, Sabina Rossi

TL;DR
This paper investigates the properties of input-consuming derivations in moded logic programs, demonstrating a weak switching lemma and providing algebraic conditions for termination, relevant for dynamic scheduling and delay constructs.
Contribution
It introduces a weak switching lemma for input-consuming derivations in nicely-moded programs and offers algebraic criteria for their termination, advancing understanding of dynamic scheduling.
Findings
Weak switching lemma holds for nicely-moded programs
Algebraic characterization of termination exists under certain conditions
Input-consuming derivations can model dynamic scheduling behaviors
Abstract
We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for input-consuming derivations. Furthermore, we show that, under suitable conditions, there exists an algebraic characterization of termination of input-consuming derivations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · semigroups and automata theory
