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

Groups > comp.lang.prolog > #14125

Biene Maya (Was: Holy Grail makes People Disappear)

Show all headers | View raw

Karel Gott - Rot und schwarz
https://www.youtube.com/watch?v=R3qAGDchWWM

So whats the fallacy in Robert Staerks modality?
It has to do with the difference between computation
and derivation, don't confuse the two!

What also helps nowadays, don't take a philosopher
on board who is totally clueless about non-classical
logics. I don't want to say names, but being that

ignorant is quite a feat. So how did Robert Staerk
start? Well he possibly had first the problem
that this here simple logic program:

p :- \+ p.

when classically translated is unsatisfiable, and
therefore in classical logic, leads to Ex Falso
Quodlibet. So they went with non-classical logic,

but a cheap one, i.e. 3-valued logic, so that
we have these two modalities:

p_s : p succeeds
p_f : p fails

The fallacy is now to think a total computable
function is the same as BIVALENCE, expressed here,
using the further modality in the game:

p_t -> p_s v p_f

non-constructive logics would immediately see
that p_s v p_f is problematic, since the above
intoduces a disjunction, without a disjunction

property. Now there is possibly the surprise
with this overall fixpoint juggling we might
have derivations that say p_t, but not in this sense:

p_t : p terminates

Just try an example with a non-continous fixpoint
operator, derived from a Clark completion. I don't
see in the slides that it is excluded?

Might even try to provide a concrete example myself...

Mild Shock schrieb:
> 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 | Next — Previous 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