Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.prolog > #14124

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

From Mild Shock <janburse@fastmail.fm>
Newsgroups comp.lang.prolog
Subject Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?]
Date 2024-08-01 19:21 +0200
Message-ID <v8gg7a$liqo$1@solani.org> (permalink)
References <v8gc6e$l44p$1@solani.org>

Show all headers | View raw


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?

Back to comp.lang.prolog | Previous | NextPrevious in thread | Next in thread | Find similar | Unroll thread


Thread

Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:13 +0200
  Alan Kay's Dynabook fueled by Prolog? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:20 +0200
    ZebralLogic for evaluating LLMs (Was: Alan Kay's Dynabook fueled by Prolog?) Mild Shock <janburse@fastmail.fm> - 2024-08-01 18:24 +0200
  Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-01 19:21 +0200
    Biene Maya (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-01 22:26 +0200
      A Challenge for Fixpoint Lovers (Was: Biene Maya) Mild Shock <janburse@fastmail.fm> - 2024-08-02 08:03 +0200
  Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-09 14:42 +0200
    Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:25 +0200
      Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 12:59 +0200
        Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:03 +0200
          Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:14 +0200
            Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:19 +0200
              Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:32 +0200
                Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:41 +0200
                Re: Is Scryer Prologs failure measurable? (Was: Holy Grail makes People Disappear) Mild Shock <janburse@fastmail.fm> - 2024-08-10 13:46 +0200
    The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:03 +0200
      Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:05 +0200
        Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 11:19 +0200
          Re: The naive reverse reality check (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-11 14:03 +0200
    How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:48 +0200
      Re: How Scryer Prolog became the disgrace of Computer Science (Was: Is Scryer Prologs failure measurable?) Mild Shock <janburse@fastmail.fm> - 2024-08-13 15:49 +0200
  Re: Holy Grail makes People Disappear [like Robert Staerk, now Ulrich Neumerkel?] Mild Shock <janburse@fastmail.fm> - 2024-08-13 09:08 +0200

csiph-web