Executable Specification of Oncology Dose-Escalation Protocols with Prolog

[dcnorris]

A long and exhilarating collaboration with Markus Triska (@triska) has yielded a paper which we have just posted to arXiv! The paper presents numerous points of interest to a diversity of perspectives:

• Those interested in system safety and verification will find here a decades-old oncology dose-escalation protocol given for the first time an executable specification, which is then used to prove various safety and liveness properties.
• Those interested in expanding the pure core of Prolog (and its applications) will find an example of applying library(reif) in a situation where otherwise recourse to (->)/2 would seem necessary. The manner in which library(clpz) has been used here, and especially its monotonic execution mode, will also be of interest.
• Those interested in dose-escalation per se will find in our regret-constrained (RC) formulation the revelation that (imperative) dose-escalation rules can emerge from more basic considerations grounded in (declared) decisional regret. Thus, we have exhibited an underlying logic to the particular protocol considered, and perhaps opened the way to development of interactive systems for designing and verifying such protocols. Furthermore, as we show toward the end of the paper, our constraint-based formulation readily accommodates certain protocol modifications that can be extremely difficult to manifest in a rampantly imperative protocol description.

We thank Ulrich Neumerkel for library(reif), so essential to our achieving a pure implementation, and @mthom for this marvelous system! We hope to develop wider collaborations in this community (and beyond) to extend this work. Although several directions for further development are already apparent to us, others may not be. So please reach out to us!

[triska]

Thank you a lot David, and congratulations!

It is a great privilege for me to contribute to these developments! This use case also perfectly illustrates the great importance of preserving reliable logical properties in Prolog programs: Saying "there are no solutions" even in cases where there are solutions can have life-threatening consequences in such safety-critical domains, where guarantees about all cases that can possibly arise must be derived. Scryer Prolog and the declarative constructs it ships with is ideally suited for writing correct Prolog programs that provide such guarantees! See also #2320 and related discussions.

I hope you all find this paper interesting, and please let us know if you have any questions or comments! Happy Valentine's Day!