A Polyvariant Binding-Time Analysis for Off-line Partial Deduction
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas (Katholieke, Universiteit Leuven, Belgium)

TL;DR
This paper presents a formal approach to binding-time analysis for logic programs, transforming on-line partial deduction into an off-line process using abstract interpretation to improve control decisions.
Contribution
It formalizes the unfolding aspect as a Prolog program and demonstrates how abstract interpretation can enable off-line partial deduction for logic programs.
Findings
Initial experiments show promising results
Formalization aids in control decision automation
Transforms on-line to off-line partial deduction
Abstract
We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we collect information about the run-time behaviour of the program. We use this information to make the control decisions about the unfolding at analysis time and to turn the on-line system into an off-line system. We report on some initial experiments.
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
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
