Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?]

Hi,
Although the work itself might be solid work.
the appeal to fixpoints should already ring a
bell. What I wish from a logic framework and
what would attract me is:
- includes the concept of a model finder,
   to show things unprovable.
- indeally a model finder, that can also
   find functions as counter models.
- allows to express things in non-classical
   logic and can make good use of non-classical logic.
- allows to express things in constructive
   function spaces and can make good use of constructive function spaces.
Currently with fixpoints and classical logic,
the approach is not enough advanced, doesn't
utilize what type theory could offer.
Bye
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?