Alan Kay's Dynabook fueled by Prolog? (Was: Holy Grail makes People Disappear)

Hi,
The paper mentions: "Huge computing power
of our modern laptops". If I look at my
new iPad Pro M4 2024, I would say
"Huge computing power of tablets", measurement
have shown it is almost twice as fast as my
laptops form ca. 2020. So lets do the following:
Bring LPTP to Dogelog Player?
Bye
P.S.: This would give a new spin of Alan
Key's vision of Dynabook. Can we run the
Dynabook idea on Prolog?
Joe Armstrong interviews Alan Kay
https://www.youtube.com/watch?v=fhOHn9TClXY
Mild Shock schrieb:

Hi,
 I remember Robert Stärk's disappearing from
academic life at ETH Zurich all of a sudden.
Did Ulrich Neumerkel now also disappeared not
 because the Scryer Prolog disaster, but after
he figured out that failure slices are not hip
enought? What could be more hip, are the modalities
 of Robert Stärk's logic more hip now and even useful?
 Automated Theorem Proving for Prolog Verification
Fred Mesnard etc.. May 2024
https://lim.univ-reunion.fr/staff/fred/Publications/24-MesnardMP-slides.pdf
 Disclaimer: I am not deep into this theory,
it has some ingredients that were floating around
the 80's / 80's, not only in the millieau of ETH Zurich,
 but also in the vincinity of Gehard Jaeger, Bern.
There are many alternative formalizations that
can express termination etc.. But maybe LPTP is
 especially suited for Prolog?