Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth


computers / comp.ai.philosophy / Re: Is this correct Prolog?

SubjectAuthor
* Is this correct Prolog?olcott
+* Re: Is this correct Prolog?Richard Damon
|+* Re: Is this correct Prolog?olcott
||`* Re: Is this correct Prolog?Richard Damon
|| `* Re: Is this correct Prolog?olcott
||  `* Re: Is this correct Prolog?Richard Damon
||   `* Re: Is this correct Prolog?olcott
||    `* Re: Is this correct Prolog?Richard Damon
||     `* Re: Is this correct Prolog?olcott
||      +* Re: Is this correct Prolog?Jeff Barnett
||      |+* Re: Is this correct Prolog?olcott
||      ||`- Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?Mr Flibble
||      | +- Re: Is this correct Prolog?polcott
||      | +- Re: Is this correct Prolog?Richard Damon
||      | `- Re: Is this correct Prolog?Jeff Barnett
||      +* Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?olcott
||      | `- Re: Is this correct Prolog?Richard Damon
||      `* Re: Is this correct Prolog?olcott
||       `* Re: Is this correct Prolog?Richard Damon
||        `* Re: Is this correct Prolog?olcott
||         `- Re: Is this correct Prolog?Richard Damon
|`* Re: Is this correct Prolog?olcott
| `* Re: Is this correct Prolog?olcott
|  +* Re: Is this correct Prolog?olcott
|  |`* Re: Is this correct Prolog?olcott
|  | `* Re: Is this correct Prolog?olcott
|  |  +- Re: Is this correct Prolog?Richard Damon
|  |  `* Re: Is this correct Prolog?olcott
|  |   `* Re: Is this correct Prolog?André G. Isaak
|  |    `* Re: Is this correct Prolog?olcott
|  |     +- Re: Is this correct Prolog?Richard Damon
|  |     `* Re: Is this correct Prolog?olcott
|  |      +* Re: Is this correct Prolog?André G. Isaak
|  |      |+* Re: Is this correct Prolog?olcott
|  |      ||+* Re: Is this correct Prolog?Richard Damon
|  |      |||`* Re: Is this correct Prolog?olcott
|  |      ||| `* Re: Is this correct Prolog?Richard Damon
|  |      |||  +- Re: Is this correct Prolog?André G. Isaak
|  |      |||  `* Re: Is this correct Prolog?olcott
|  |      |||   `* Re: Is this correct Prolog?Richard Damon
|  |      |||    `* Re: Is this correct Prolog?olcott
|  |      |||     `* Re: Is this correct Prolog?Richard Damon
|  |      |||      `* Re: Is this correct Prolog?olcott
|  |      |||       +- Re: Is this correct Prolog?André G. Isaak
|  |      |||       `* Re: Is this correct Prolog?Richard Damon
|  |      |||        `* Re: Is this correct Prolog?olcott
|  |      |||         +- Re: Is this correct Prolog?André G. Isaak
|  |      |||         `* Re: Is this correct Prolog?Richard Damon
|  |      |||          `* Re: Is this correct Prolog?olcott
|  |      |||           `- Re: Is this correct Prolog?Richard Damon
|  |      ||`* Re: Is this correct Prolog?André G. Isaak
|  |      || +* Re: Is this correct Prolog?olcott
|  |      || |`* Re: Is this correct Prolog?André G. Isaak
|  |      || | `* Re: Is this correct Prolog? [ André is provenolcott
|  |      || |  `* Re: Is this correct Prolog? [ André is provenAndré G. Isaak
|  |      || |   `- Re: Is this correct Prolog? [ André is provenolcott
|  |      || `* Re: Is this correct Prolog? [ André is provenolcott
|  |      ||  `* Re: Is this correct Prolog? [ André is provenRichard Damon
|  |      ||   `- Re: Is this correct Prolog? [ André is provenolcott
|  |      |`- Re: Is this correct Prolog?olcott
|  |      `- Re: Is this correct Prolog?Richard Damon
|  `* Re: Is this correct Prolog?olcott
|   `- Re: Is this correct Prolog?André G. Isaak
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Richard Damon
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Richard Damon
|   `* Re: Is this correct Prolog?olcott
|    `- Re: Is this correct Prolog?Richard Damon
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Aleksy Grabowski
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Aleksy Grabowski
|   `* Re: Is this correct Prolog?olcott
|    `* Re: Is this correct Prolog?Aleksy Grabowski
|     `* Re: Is this correct Prolog?olcott
|      +* Re: Is this correct Prolog?Aleksy Grabowski
|      |`* Re: Is this correct Prolog?olcott
|      | `* Re: Is this correct Prolog?Aleksy Grabowski
|      |  `- Re: Is this correct Prolog?olcott
|      `* Re: Is this correct Prolog?Jeff Barnett
|       +* Re: Is this correct Prolog?Mr Flibble
|       |`- Re: Is this correct Prolog?olcott
|       `* Re: Is this correct Prolog?olcott
|        `* Re: Is this correct Prolog?Richard Damon
|         `* Re: Is this correct Prolog?Aleksy Grabowski
|          +* Re: Is this correct Prolog?Ben
|          |`* Re: Is this correct Prolog?olcott
|          | +* Re: Is this correct Prolog?Ben
|          | |`* Re: Is this correct Prolog?olcott
|          | | +* Re: Is this correct Prolog?Richard Damon
|          | | |`* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | | `* Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  +* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | |  |`- Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  `- Re: Is this correct Prolog? [ Tarski ]olcott
|          | | `- Re: Is this correct Prolog?Ben
|          | `* Re: Is this correct Prolog?André G. Isaak
|          |  +* Re: Is this correct Prolog?olcott
|          |  `* Re: Is this correct Prolog?Jeff Barnett
|          `* Re: Is this correct Prolog?olcott
`* Re: Is this correct Prolog?olcott

Pages:123456
Is this correct Prolog?

<qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8498&group=comp.ai.philosophy#8498

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!nntp.club.cc.cmu.edu!45.76.7.193.MISMATCH!3.us.feeder.erje.net!feeder.erje.net!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 02:02:22 -0500
Date: Sat, 30 Apr 2022 02:02:23 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Content-Language: en-US
From: NoO...@NoWhere.com (olcott)
Subject: Is this correct Prolog?
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 20
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-4tUH4ujlpKqjc8OQZrSKEFphvvw0HBX+idZ/AFZ5zzYAmz7Q1tUBT/Do2Q0j2pXtkIKiq10eZBPZHEl!f/ll6I/z1XNSXwrUjz6+fXBpOw4463nW/dNLnlBqXF1J73AjmCRlsAilkJ6Na9RjpzIyCvN4QH4=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 1579
 by: olcott - Sat, 30 Apr 2022 07:02 UTC

LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<I4lbK.452483$t2Bb.96330@fx98.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8503&group=comp.ai.philosophy#8503

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx98.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 30
Message-ID: <I4lbK.452483$t2Bb.96330@fx98.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sat, 30 Apr 2022 21:08:57 -0400
X-Received-Bytes: 1848
 by: Richard Damon - Sun, 1 May 2022 01:08 UTC

On 4/30/22 3:02 AM, olcott wrote:
> LP := ~True(LP) is translated to Prolog:
>
> ?- LP = not(true(LP)).
> LP = not(true(LP)).
>
> ?- unify_with_occurs_check(LP, not(true(LP))).
> false.
>
> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>
> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>
>
>

Since it isn't giving you a "syntax error", it is probably correct
Prolog. Not sure if your interpretation of the results is correct.

All that false means is that the statement

LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due to its
limited logic rules.

I will condition this answer on the fact that I am not a prolog
specialist, but just reading the manual and providing basic
understanding, which I am not sure of your ability to do so.

Re: Is this correct Prolog?

<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8504&group=comp.ai.philosophy#8504

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 20:42:10 -0500
Date: Sat, 30 Apr 2022 20:42:10 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <I4lbK.452483$t2Bb.96330@fx98.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 53
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-79uIe4iNDrH6rzZhMh63WyBEn6mAHe+2X9KwpjWfgH1pGgBfgrJTaWp+3vamDwq/ScxyiVrt/Hbecii!zXvunNLBYmRjw1gHUK2ToLk11HVXYeue+2Wucw7lbyvXsDJDGldohQ34oc7q+JFCIMcwINKHv5I=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2867
 by: olcott - Sun, 1 May 2022 01:42 UTC

On 4/30/2022 8:08 PM, Richard Damon wrote:
> On 4/30/22 3:02 AM, olcott wrote:
>> LP := ~True(LP) is translated to Prolog:
>>
>> ?- LP = not(true(LP)).
>> LP = not(true(LP)).
>>
>> ?- unify_with_occurs_check(LP, not(true(LP))).
>> false.
>>
>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>
>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>
>>
>>
>
> Since it isn't giving you a "syntax error", it is probably correct
> Prolog. Not sure if your interpretation of the results is correct.
>
> All that false means is that the statement
>
>
> LP = not(true(LP))
>
> is recursive and that Prolog can't actually evaluate it due to its
> limited logic rules.
>

That is not what Clocksin & Mellish says. They say it is an erroneous
"infinite term" meaning that it specifies infinitely nested definition
like this:

LP := ~True(LP) specifies:
~True(~True(~True(L~True(L~True(...))
The ellipses "..." mean "on and on forever"

One half a page of the Clocksin & Mellish text is quoted on page (3) of
my paper:

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

> I will condition this answer on the fact that I am not a prolog
> specialist, but just reading the manual and providing basic
> understanding, which I am not sure of your ability to do so.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8505&group=comp.ai.philosophy#8505

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 20:47:43 -0500
Date: Sat, 30 Apr 2022 20:47:42 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <I4lbK.452483$t2Bb.96330@fx98.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 33
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-HAmws2l4OR4McBL08LHZyKMou14aVG2v1u21HDee/M95GTafNM2HDzs3oN7tbiCO/gQONUUVaFRC9j4!POcj1dbJ0t5k5TmspvLRlcsE9DbTTMSS4Mimn6f1i+N92Z7lnyQYpCelRTlHu97M36w05Xw6QXI=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2253
 by: olcott - Sun, 1 May 2022 01:47 UTC

On 4/30/2022 8:08 PM, Richard Damon wrote:
> On 4/30/22 3:02 AM, olcott wrote:
>> LP := ~True(LP) is translated to Prolog:
>>
>> ?- LP = not(true(LP)).
>> LP = not(true(LP)).
>>
>> ?- unify_with_occurs_check(LP, not(true(LP))).
>> false.
>>
>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>
>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>
>>
>>
>
> Since it isn't giving you a "syntax error", it is probably correct
> Prolog. Not sure if your interpretation of the results is correct.

I asked the question incorrectly, what I really needed to know is
whether or not the Prolog correctly encodes this logic sentence:
LP := ~True(LP)

x := y means x is defined to be another name for y
https://en.wikipedia.org/wiki/List_of_logic_symbols

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<AQlbK.11129$lX6b.2320@fx33.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8506&group=comp.ai.philosophy#8506

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx33.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 66
Message-ID: <AQlbK.11129$lX6b.2320@fx33.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sat, 30 Apr 2022 22:00:00 -0400
X-Received-Bytes: 3234
X-Original-Bytes: 3101
 by: Richard Damon - Sun, 1 May 2022 02:00 UTC

On 4/30/22 9:42 PM, olcott wrote:
> On 4/30/2022 8:08 PM, Richard Damon wrote:
>> On 4/30/22 3:02 AM, olcott wrote:
>>> LP := ~True(LP) is translated to Prolog:
>>>
>>> ?- LP = not(true(LP)).
>>> LP = not(true(LP)).
>>>
>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>> false.
>>>
>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>
>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>
>>>
>>>
>>
>> Since it isn't giving you a "syntax error", it is probably correct
>> Prolog. Not sure if your interpretation of the results is correct.
>>
>> All that false means is that the statement
>>
>>
>> LP = not(true(LP))
>>
>> is recursive and that Prolog can't actually evaluate it due to its
>> limited logic rules.
>>
>
> That is not what Clocksin & Mellish says. They say it is an erroneous
> "infinite term" meaning that it specifies infinitely nested definition
> like this:

No, that IS what they say, that this sort of recursion fails the test of
Unification, not that it is has no possible logical meaning.

Prolog represents a somewhat basic form of logic, useful for many cases,
but not encompassing all possible reasoning systems.

Maybe it can handle every one that YOU can understand, but it can't
handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial for an
unknown value can lead to an infinite expansion, but the factorial is
well defined for all positive integers. The fact that a "prolog like"
expansion operator might not be able to handle the definition, doesn't
mean it doesn't have meaning.

>
> LP := ~True(LP) specifies:
> ~True(~True(~True(L~True(L~True(...))
> The ellipses "..." mean "on and on forever"
>
> One half a page of the Clocksin & Mellish text is quoted on page (3) of
> my paper:
>
> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>
>
>> I will condition this answer on the fact that I am not a prolog
>> specialist, but just reading the manual and providing basic
>> understanding, which I am not sure of your ability to do so.
>
>

Re: Is this correct Prolog?

<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8507&group=comp.ai.philosophy#8507

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 21:21:24 -0500
Date: Sat, 30 Apr 2022 21:21:24 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <AQlbK.11129$lX6b.2320@fx33.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
Lines: 82
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-6bn6xqwdSR7b5Pwlb69C7ZtdioYbZhYb31i6OGSoM8q7YYLEFMwebZPB4533vIDl3iR5t4vrAcMf4N2!yB3lprQnIgUy5nwxhZl0HSMOV6VPgSyRBQmpj8Lz564f5Bk+q6GnaFuVoPqBuJnx6af1P+YNVFw=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4072
 by: olcott - Sun, 1 May 2022 02:21 UTC

On 4/30/2022 9:00 PM, Richard Damon wrote:
> On 4/30/22 9:42 PM, olcott wrote:
>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>> On 4/30/22 3:02 AM, olcott wrote:
>>>> LP := ~True(LP) is translated to Prolog:
>>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>>
>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>
>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>
>>>>
>>>>
>>>
>>> Since it isn't giving you a "syntax error", it is probably correct
>>> Prolog. Not sure if your interpretation of the results is correct.
>>>
>>> All that false means is that the statement
>>>
>>>
>>> LP = not(true(LP))
>>>
>>> is recursive and that Prolog can't actually evaluate it due to its
>>> limited logic rules.
>>>
>>
>> That is not what Clocksin & Mellish says. They say it is an erroneous
>> "infinite term" meaning that it specifies infinitely nested definition
>> like this:
>
> No, that IS what they say, that this sort of recursion fails the test of
> Unification, not that it is has no possible logical meaning.
>
> Prolog represents a somewhat basic form of logic, useful for many cases,
> but not encompassing all possible reasoning systems.
>
> Maybe it can handle every one that YOU can understand, but it can't
> handle many higher order logical structures.
>
> Note, for instance, at least some ways of writing factorial for an
> unknown value can lead to an infinite expansion, but the factorial is
> well defined for all positive integers. The fact that a "prolog like"
> expansion operator might not be able to handle the definition, doesn't
> mean it doesn't have meaning.
>

It is really dumb that you continue to take wild guesses again the
verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text and
eliminate your ignorance.

>>
>> LP := ~True(LP) specifies:
>> ~True(~True(~True(L~True(L~True(...))
>> The ellipses "..." mean "on and on forever"
>>
>> One half a page of the Clocksin & Mellish text is quoted on page (3)
>> of my paper:
>>
>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>
>>
>>> I will condition this answer on the fact that I am not a prolog
>>> specialist, but just reading the manual and providing basic
>>> understanding, which I am not sure of your ability to do so.
>>
>>
>

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<uombK.379436$Gojc.287190@fx99.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8509&group=comp.ai.philosophy#8509

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx99.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 84
Message-ID: <uombK.379436$Gojc.287190@fx99.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sat, 30 Apr 2022 22:38:19 -0400
X-Received-Bytes: 4442
 by: Richard Damon - Sun, 1 May 2022 02:38 UTC

On 4/30/22 10:21 PM, olcott wrote:
> On 4/30/2022 9:00 PM, Richard Damon wrote:
>> On 4/30/22 9:42 PM, olcott wrote:
>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>
>>>>> ?- LP = not(true(LP)).
>>>>> LP = not(true(LP)).
>>>>>
>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>> false.
>>>>>
>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>
>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>
>>>>>
>>>>>
>>>>
>>>> Since it isn't giving you a "syntax error", it is probably correct
>>>> Prolog. Not sure if your interpretation of the results is correct.
>>>>
>>>> All that false means is that the statement
>>>>
>>>>
>>>> LP = not(true(LP))
>>>>
>>>> is recursive and that Prolog can't actually evaluate it due to its
>>>> limited logic rules.
>>>>
>>>
>>> That is not what Clocksin & Mellish says. They say it is an erroneous
>>> "infinite term" meaning that it specifies infinitely nested
>>> definition like this:
>>
>> No, that IS what they say, that this sort of recursion fails the test
>> of Unification, not that it is has no possible logical meaning.
>>
>> Prolog represents a somewhat basic form of logic, useful for many
>> cases, but not encompassing all possible reasoning systems.
>>
>> Maybe it can handle every one that YOU can understand, but it can't
>> handle many higher order logical structures.
>>
>> Note, for instance, at least some ways of writing factorial for an
>> unknown value can lead to an infinite expansion, but the factorial is
>> well defined for all positive integers. The fact that a "prolog like"
>> expansion operator might not be able to handle the definition, doesn't
>> mean it doesn't have meaning.
>>
>
> It is really dumb that you continue to take wild guesses again the
> verified facts.
>
> Please read the Clocksin & Mellish (on page 3 of my paper) text and
> eliminate your ignorance.
>

I did. You just don't seem to understand what I am saying because it is
above your head.

Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of those
statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it doesn't
have a logical meaning, only that it doesn't have a logical meaning in
Prolog.

The inability of Prolog to "Unify" the expression, does not mean the
expression doesn't have logical meaning, just that PROLOG can't derive
meaning from the expression.

The Halting Problem and the incompleteness proofs never claims that they
is designed for the subset of logic that is Prolog, and in fact they may
be implicitly denying that, as I don't think Prolog handles enough
complexity of logic to reach the threshold needed to express "G" in
Godel's proof. (Your need to "simplify" it, is indicative of this, and
shows you don't understand the actual proof).

This means that the fact that Prolog rejects unification of the
statements doesn't actually say that much, just that the statement isn't
of the type that Prolog can fully process.

Re: Is this correct Prolog?

<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8510&group=comp.ai.philosophy#8510

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 21:56:56 -0500
Date: Sat, 30 Apr 2022 21:56:55 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <uombK.379436$Gojc.287190@fx99.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 99
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-ShbY2xUzencpMY3nw2pzUs1O1OaaWGMTOnEpHCNOeKV+0ifyuDGxfWigRcj/yaH9OJMLO/I/aLUJlfu!rft8dhVEDkk7igPDU2vq3koSYHrrHtDdPiTT/6MK1FA2wxwlhTgK2Qj7CMdUp5Q7KibRk2xTuWU=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5197
 by: olcott - Sun, 1 May 2022 02:56 UTC

On 4/30/2022 9:38 PM, Richard Damon wrote:
> On 4/30/22 10:21 PM, olcott wrote:
>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>> On 4/30/22 9:42 PM, olcott wrote:
>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>
>>>>>> ?- LP = not(true(LP)).
>>>>>> LP = not(true(LP)).
>>>>>>
>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>> false.
>>>>>>
>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>
>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>> Since it isn't giving you a "syntax error", it is probably correct
>>>>> Prolog. Not sure if your interpretation of the results is correct.
>>>>>
>>>>> All that false means is that the statement
>>>>>
>>>>>
>>>>> LP = not(true(LP))
>>>>>
>>>>> is recursive and that Prolog can't actually evaluate it due to its
>>>>> limited logic rules.
>>>>>
>>>>
>>>> That is not what Clocksin & Mellish says. They say it is an
>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>> nested definition like this:
>>>
>>> No, that IS what they say, that this sort of recursion fails the test
>>> of Unification, not that it is has no possible logical meaning.
>>>
>>> Prolog represents a somewhat basic form of logic, useful for many
>>> cases, but not encompassing all possible reasoning systems.
>>>
>>> Maybe it can handle every one that YOU can understand, but it can't
>>> handle many higher order logical structures.
>>>
>>> Note, for instance, at least some ways of writing factorial for an
>>> unknown value can lead to an infinite expansion, but the factorial is
>>> well defined for all positive integers. The fact that a "prolog like"
>>> expansion operator might not be able to handle the definition,
>>> doesn't mean it doesn't have meaning.
>>>
>>
>> It is really dumb that you continue to take wild guesses again the
>> verified facts.
>>
>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>> eliminate your ignorance.
>>
>
> I did. You just don't seem to understand what I am saying because it is
> above your head.
>
> Prolog is NOT the defining authority for what is a valid logical
> statement, but a system of programming to handle a subset of those
> statements (a useful subset, but a subset).
>
> The fact that Prolog doesn't allow something doesn't mean it doesn't
> have a logical meaning, only that it doesn't have a logical meaning in
> Prolog.
In this case it does. I have spent thousands of hours on the semantic
error of infinitely recursive definition and written a dozen papers on
it. Glancing at one of two of the words of Clocksin & Mellish does not
count as reading it.

BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:

equal(X, X).?-
equal(foo(Y), Y).

that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<VTmbK.655548$mF2.416033@fx11.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8511&group=comp.ai.philosophy#8511

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!newsfeed.xs4all.nl!newsfeed8.news.xs4all.nl!peer01.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx11.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 124
Message-ID: <VTmbK.655548$mF2.416033@fx11.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sat, 30 Apr 2022 23:11:50 -0400
X-Received-Bytes: 6267
 by: Richard Damon - Sun, 1 May 2022 03:11 UTC

On 4/30/22 10:56 PM, olcott wrote:
> On 4/30/2022 9:38 PM, Richard Damon wrote:
>> On 4/30/22 10:21 PM, olcott wrote:
>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>
>>>>>>> ?- LP = not(true(LP)).
>>>>>>> LP = not(true(LP)).
>>>>>>>
>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>> false.
>>>>>>>
>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>
>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> Since it isn't giving you a "syntax error", it is probably correct
>>>>>> Prolog. Not sure if your interpretation of the results is correct.
>>>>>>
>>>>>> All that false means is that the statement
>>>>>>
>>>>>>
>>>>>> LP = not(true(LP))
>>>>>>
>>>>>> is recursive and that Prolog can't actually evaluate it due to its
>>>>>> limited logic rules.
>>>>>>
>>>>>
>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>> nested definition like this:
>>>>
>>>> No, that IS what they say, that this sort of recursion fails the
>>>> test of Unification, not that it is has no possible logical meaning.
>>>>
>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>> cases, but not encompassing all possible reasoning systems.
>>>>
>>>> Maybe it can handle every one that YOU can understand, but it can't
>>>> handle many higher order logical structures.
>>>>
>>>> Note, for instance, at least some ways of writing factorial for an
>>>> unknown value can lead to an infinite expansion, but the factorial
>>>> is well defined for all positive integers. The fact that a "prolog
>>>> like" expansion operator might not be able to handle the definition,
>>>> doesn't mean it doesn't have meaning.
>>>>
>>>
>>> It is really dumb that you continue to take wild guesses again the
>>> verified facts.
>>>
>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>>> eliminate your ignorance.
>>>
>>
>> I did. You just don't seem to understand what I am saying because it
>> is above your head.
>>
>> Prolog is NOT the defining authority for what is a valid logical
>> statement, but a system of programming to handle a subset of those
>> statements (a useful subset, but a subset).
>>
>> The fact that Prolog doesn't allow something doesn't mean it doesn't
>> have a logical meaning, only that it doesn't have a logical meaning in
>> Prolog.
> In this case it does. I have spent thousands of hours on the semantic
> error of infinitely recursive definition and written a dozen papers on
> it. Glancing at one of two of the words of Clocksin & Mellish does not
> count as reading it.

And it appears that you don't understand it, because you still make
category errors when trying to talk about it.

>
> BEGIN:(Clocksin & Mellish 2003:254)
> Finally, a note about how Prolog matching sometimes differs from the
> unification used in Resolution. Most Prolog systems will allow you to
> satisfy goals like:
>
>   equal(X, X).?-
>   equal(foo(Y), Y).
>
> that is, they will allow you to match a term against an uninstantiated
> subterm of itself. In this example, foo(Y) is matched against Y, which
> appears within it. As a result, Y will stand for foo(Y), which is
> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
> and so on. So Y ends up standing for some kind of infinite structure.
> END:(Clocksin & Mellish 2003:254)
>
> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>

Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

if naively expanded has an infinite expansion.

But, based on mathematical knowledge, and can actually be proven from
the definition, something like Fact(n+1)/fact(n), even for an unknown n,
can be reduced without the need to actually expend infinite operations.

Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
abort its simulation, then for THAT H^, we have that H^(H^) is
non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a
counter example

When you program H to abort its simulation of H^ at some point, and
build your H^ on that H, then H(H^,H^), will return the non-halting
answer, and H^(H^) when PROPERLY run or simulated halts, because H has
the same "cut off" logic at the factorial above.

The naive expansion thinks it is infinite, but the correct expansion
sees the cut off and sees that it is actually finite.

Re: Is this correct Prolog?

<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8512&group=comp.ai.philosophy#8512

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 22:15:57 -0500
Date: Sat, 30 Apr 2022 22:15:56 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <VTmbK.655548$mF2.416033@fx11.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 111
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-gAYd8L2gER0atQZ3a3jslb+kylQAagF3iYW8t4G5tyaA64oO8sHAXWIDRqqRvT4AXe09UHJTkqR6aZp!trWQPCgBF81Lv1xLuca2Mrq9CT65a5CJ0j1/1MLHb5fRSZcTlyEG1raITVrwpFk1T93KDLawJGk=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5961
 by: olcott - Sun, 1 May 2022 03:15 UTC

On 4/30/2022 10:11 PM, Richard Damon wrote:
> On 4/30/22 10:56 PM, olcott wrote:
>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>> On 4/30/22 10:21 PM, olcott wrote:
>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>
>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>> LP = not(true(LP)).
>>>>>>>>
>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>> false.
>>>>>>>>
>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>
>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>> correct Prolog. Not sure if your interpretation of the results is
>>>>>>> correct.
>>>>>>>
>>>>>>> All that false means is that the statement
>>>>>>>
>>>>>>>
>>>>>>> LP = not(true(LP))
>>>>>>>
>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>> its limited logic rules.
>>>>>>>
>>>>>>
>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>> nested definition like this:
>>>>>
>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>
>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>
>>>>> Maybe it can handle every one that YOU can understand, but it can't
>>>>> handle many higher order logical structures.
>>>>>
>>>>> Note, for instance, at least some ways of writing factorial for an
>>>>> unknown value can lead to an infinite expansion, but the factorial
>>>>> is well defined for all positive integers. The fact that a "prolog
>>>>> like" expansion operator might not be able to handle the
>>>>> definition, doesn't mean it doesn't have meaning.
>>>>>
>>>>
>>>> It is really dumb that you continue to take wild guesses again the
>>>> verified facts.
>>>>
>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>>>> eliminate your ignorance.
>>>>
>>>
>>> I did. You just don't seem to understand what I am saying because it
>>> is above your head.
>>>
>>> Prolog is NOT the defining authority for what is a valid logical
>>> statement, but a system of programming to handle a subset of those
>>> statements (a useful subset, but a subset).
>>>
>>> The fact that Prolog doesn't allow something doesn't mean it doesn't
>>> have a logical meaning, only that it doesn't have a logical meaning
>>> in Prolog.
>> In this case it does. I have spent thousands of hours on the semantic
>> error of infinitely recursive definition and written a dozen papers on
>> it. Glancing at one of two of the words of Clocksin & Mellish does not
>> count as reading it.
>
> And it appears that you don't understand it, because you still make
> category errors when trying to talk about it.
>
>>
>> BEGIN:(Clocksin & Mellish 2003:254)
>> Finally, a note about how Prolog matching sometimes differs from the
>> unification used in Resolution. Most Prolog systems will allow you to
>> satisfy goals like:
>>
>>    equal(X, X).?-
>>    equal(foo(Y), Y).
>>
>> that is, they will allow you to match a term against an uninstantiated
>> subterm of itself. In this example, foo(Y) is matched against Y, which
>> appears within it. As a result, Y will stand for foo(Y), which is
>> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
>> and so on. So Y ends up standing for some kind of infinite structure.
>> END:(Clocksin & Mellish 2003:254)
>>
>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>
>
> Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can possibly
prove any infinite expression. It is the same thing as a program that is
stuck in an infinite loop.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8513&group=comp.ai.philosophy#8513

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 30 Apr 2022 23:49:14 -0500
Date: Sat, 30 Apr 2022 23:49:13 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4kp78$vuc$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 47
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-C2NSBYQaVPsx0rD6/ELdFbiGMHQ/BCH6etukVxAyJmFnaZPgTAIO8+LNnosLfEYzN690OtDdunScgBh!+qSNxnOtXjF/ZEzZfYD5lqyPy5AEWmrY+ih0V6KqM0VgidAAOEOmk0YjPVhFqUz4EE3x0g8buV4=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2604
 by: olcott - Sun, 1 May 2022 04:49 UTC

On 4/30/2022 8:53 PM, André G. Isaak wrote:
> On 2022-04-30 19:47, olcott wrote:
>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>> On 4/30/22 3:02 AM, olcott wrote:
>>>> LP := ~True(LP) is translated to Prolog:
>>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>>
>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>
>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>
>>>>
>>>>
>>>
>>> Since it isn't giving you a "syntax error", it is probably correct
>>> Prolog. Not sure if your interpretation of the results is correct.
>>
>> I asked the question incorrectly, what I really needed to know is
>> whether or not the Prolog correctly encodes this logic sentence:
>> LP := ~True(LP)
>
> Since that isn't a 'logic sentence', no one can answer this.
>
> André
>
>

What about this one?
LP ↔ ¬True(LP) // Tarski uses something like this
https://liarparadox.org/Tarski_275_276.pdf

or this one?
G ↔ ¬(F ⊢ G)

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<t4l5hq$8bi$1@dont-email.me>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8514&group=comp.ai.philosophy#8514

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: jbb...@notatt.com (Jeff Barnett)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sat, 30 Apr 2022 23:24:05 -0600
Organization: A noiseless patient Spider
Lines: 156
Message-ID: <t4l5hq$8bi$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: base64
Injection-Date: Sun, 1 May 2022 05:24:11 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="dfa4a43240a45544272de93b7ef2f48d";
logging-data="8562"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/kom2tSXfB15c3Ezh7IEqUg0UtsW7Wgrk="
User-Agent: Mozilla/5.0 (Windows NT 6.1; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:G9lxvRrQvhnluE8MUUhkWYoaoJY=
In-Reply-To: <Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
Content-Language: en-US
 by: Jeff Barnett - Sun, 1 May 2022 05:24 UTC

On 4/30/2022 9:15 PM, olcott wrote:
> On 4/30/2022 10:11 PM, Richard Damon wrote:
>> On 4/30/22 10:56 PM, olcott wrote:
>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>
>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>
>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>> false.
>>>>>>>>>
>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>
>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>> is correct.
>>>>>>>>
>>>>>>>> All that false means is that the statement
>>>>>>>>
>>>>>>>>
>>>>>>>> LP = not(true(LP))
>>>>>>>>
>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>> its limited logic rules.
>>>>>>>>
>>>>>>>
>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>> nested definition like this:
>>>>>>
>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>
>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>
>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>> can't handle many higher order logical structures.
>>>>>>
>>>>>> Note, for instance, at least some ways of writing factorial for an
>>>>>> unknown value can lead to an infinite expansion, but the factorial
>>>>>> is well defined for all positive integers. The fact that a "prolog
>>>>>> like" expansion operator might not be able to handle the
>>>>>> definition, doesn't mean it doesn't have meaning.
>>>>>>
>>>>>
>>>>> It is really dumb that you continue to take wild guesses again the
>>>>> verified facts.
>>>>>
>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>>>>> eliminate your ignorance.
>>>>>
>>>>
>>>> I did. You just don't seem to understand what I am saying because it
>>>> is above your head.
>>>>
>>>> Prolog is NOT the defining authority for what is a valid logical
>>>> statement, but a system of programming to handle a subset of those
>>>> statements (a useful subset, but a subset).
>>>>
>>>> The fact that Prolog doesn't allow something doesn't mean it doesn't
>>>> have a logical meaning, only that it doesn't have a logical meaning
>>>> in Prolog.
>>> In this case it does. I have spent thousands of hours on the semantic
>>> error of infinitely recursive definition and written a dozen papers
>>> on it. Glancing at one of two of the words of Clocksin & Mellish does
>>> not count as reading it.
>>
>> And it appears that you don't understand it, because you still make
>> category errors when trying to talk about it.
>>
>>>
>>> BEGIN:(Clocksin & Mellish 2003:254)
>>> Finally, a note about how Prolog matching sometimes differs from the
>>> unification used in Resolution. Most Prolog systems will allow you to
>>> satisfy goals like:
>>>
>>>    equal(X, X).?-
>>>    equal(foo(Y), Y).
>>>
>>> that is, they will allow you to match a term against an
>>> uninstantiated subterm of itself. In this example, foo(Y) is matched
>>> against Y, which appears within it. As a result, Y will stand for
>>> foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is
>>> foo(foo(foo(Y))), and so on. So Y ends up standing for some kind of
>>> infinite structure.
>>> END:(Clocksin & Mellish 2003:254)
>>>
>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>
>>
>> Right. but some infinite structures might actually have meaning.
> Not in this case, it is very obvious that no theorem prover can possibly
> prove any infinite expression. It is the same thing as a program that is
> stuck in an infinite loop.
Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.
Just like:
Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
if naively expanded has an infinite expansion.
But, based on mathematical knowledge, and can actually be proven from
the definition, something like Fact(n+1)/fact(n), even for an unknown n,
can be reduced without the need to actually expend infinite operations.
Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
abort its simulation, then for THAT H^, we have that H^(H^) is
non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a
counter example
When you program H to abort its simulation of H^ at some point, and
build your H^ on that H, then H(H^,H^), will return the non-halting
answer, and H^(H^) when PROPERLY run or simulated halts, because H has
the same "cut off" logic at the factorial above.
The naive expansion thinks it is infinite, but the correct expansion
sees the cut off and sees that it is actually finite.
----------------------------------------------------------------------
A good symbolic manipulation system or a theorem prover with appropriate
axioms and rules of inference could surely handle forms such as
Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant
fool, who seems to think that the unthinking infinite unrolling of a
form must occur. Only you would think that a solver system would
completely unroll a form before analyzing it and applying
transformations to it.
Son, it don't work that way (unless you are defining and making a mess
trying to write the system yourself). Systems usually have rules that
make small incremental transformations and usually search breadth first
with perhaps a limited amount of depth first interludes. If they don't
use a breadth first strategy, they will not be able to claim the
completeness property. (See resolution theorem prover literature for
some explanation. You wont understand it but you can cite as if you did!)
Richard was trying to explain this to you in the snipped portion I
recited just above. Question for Peter holding his pecker: How do you
always and I mean always manage to delete the part of a message you
respond too that addresses the point you now try to make?
A typically subsequence you might see in the trace: would include in
order but not necessarily consecutively:
Fact(n+1)/Fact(n)
(n+1)*Fact(n)/Fact(n)
(n+1)
Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found
too. In some circumstances, these other terms might be helpful. A
theorem prover or manipulator does all of this, breadth first, hoping to
blindly stumble on a solution. You can provide heuristics that might
speed up the process but no advice short of an oracle will get you even
one more result. (Another manifestation of HP.) It's the slow grinding
through the possibilities that guarantees that if a result can be found,
it will be found. And all the theory that you don't understand says
that's the best you can do.

Click here to read the complete article

Re: Is this correct Prolog?

<KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8521&group=comp.ai.philosophy#8521

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 05:58:26 -0500
Date: Sun, 1 May 2022 05:58:25 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<t4ljjp$4ph$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4ljjp$4ph$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 51
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-SBAm64I5f2q0oOHoFESkzc179+UHn9ucRUZCcnm6kIc+Lj/80IM8WTRdYGupMWxqnsqWI8MqOaKMeUs!WyatgCcZ7XjKSFE/3Tc3l8XBJBpE19dM5uaFF10robcmcwwn+Ink51ptpq6uBgaaL8AFJ5hlE3o=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3195
 by: olcott - Sun, 1 May 2022 10:58 UTC

On 5/1/2022 4:24 AM, Mikko wrote:
> On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:
>
>> I just want to add some small note.
>>
>> This "not(true(_))" thing is misleading.
>> Please note that it is *not* a negation.
>> Functionally it is equivalent to:
>>
>> X = foo(bar(X)).
>
> That's correct. Prolog language does not give any inherent semantics to
> data structures. It only defines the execution semantics of language
> structures and standard library symbols. Those same synbols can be used
> in data structures with entirely different purposes.
>
> Mikko
>

negation, not, \+
The concept of logical negation in Prolog is problematical, in the sense
that the only method that Prolog can use to tell if a proposition is
false is to try to prove it (from the facts and rules that it has been
told about), and then if this attempt fails, it concludes that the
proposition is false. This is referred to as negation as failure.

http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
This is actually a superior model to convention logic in that it only
seeks to prove not true, thus detects expressions of language that are
simply not truth bearers.

Expressions of (formal or natural) language that can possibly be
resolved to a truth value are [truth bearers].

There are only two ways that an expression of language can be resolved
to a truth value:
(1) An expression of language is assigned a truth value such as "cats
are animals" is defined to be true.

(2) Truth preserving operations are applied to expressions of language
that are known to be true. {cats are animals} and {animals are living
things} therefore {cats are living things}. Copyright 2021 PL Olcott

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8522&group=comp.ai.philosophy#8522

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:00:29 -0500
Date: Sun, 1 May 2022 06:00:28 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4ljnn$5k0$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 25
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-YPGjyuzB/VJ978g30oT6rTD7cm0A5srqCJaad1OLYYegIdj3HgDjGYv2jHs/ueUv5LZ7CSmCQi1h0Pu!GFu8j+z9fyKYWrEpaPwy7vkFzwg91LRSQAnq4kjxsyr1o7WD+dQwCtuJjEhoPFadVkrMX3qsoqM=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2144
 by: olcott - Sun, 1 May 2022 11:00 UTC

On 5/1/2022 4:26 AM, Mikko wrote:
> On 2022-04-30 21:08:05 +0000, olcott said:
>
>> negation, not, \+
>> The concept of logical negation in Prolog is problematical, in the
>> sense that the only method that Prolog can use to tell if a
>> proposition is false is to try to prove it (from the facts and rules
>> that it has been told about), and then if this attempt fails, it
>> concludes that the proposition is false. This is referred to as
>> negation as failure.
>
> Note that the negation discussed above is not present in LP =
> not(true(LP)).
>
> Mikko
>

Is says that it is. It says that "not" is synonymous with \+.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8523&group=comp.ai.philosophy#8523

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:06:24 -0500
Date: Sun, 1 May 2022 06:06:23 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4lkei$acm$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
Lines: 60
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-rwIZ8Z3OCuwgfV64wQIoRUNU8WuxxBkGGPoiArM23NsOQK/8nMYiScHVeKHxizXQG5WPhQWBbj5nJ2s!0CF6TbZGK5P5rH0aB9pwfo8Ig0T0uJizVdVDgqYPJ0nSPAPgkOZlNIrmxHa6PfFgsZrr/DHr74Y=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3241
 by: olcott - Sun, 1 May 2022 11:06 UTC

On 5/1/2022 4:38 AM, Mikko wrote:
> On 2022-04-30 20:48:47 +0000, olcott said:
>
>> On 4/30/2022 4:31 AM, Mikko wrote:
>>> On 2022-04-30 07:02:23 +0000, olcott said:
>>>
>>>> LP := ~True(LP) is translated to Prolog:
>>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>
>>> This is correct but to fail would also be correct.
>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>
>>> unify_with_occurs_check must fail if the unified data structure
>>> would contain loops.
>>>
>>> Mikko
>>>
>>
>> The above is the actual execution of actual Prolog code using
>> (SWI-Prolog (threaded, 64 bits, version 7.6.4).
>
> Another Prolog implementation might interprete LP = not(true(LP))
> differently
> and still conform to the prolog standard.
>
>> According to Clocksin & Mellish it is not a mere loop, it is an
>> "infinite term" thus infinitely recursive definition.
>
> When discussing data structures, "infinite" and "loop" mean the same.
> The data structure is infinitely deep but contains only finitely many
> distinct objects and occupies only a finite amount of memory.
>

That is incorrect. any structure that is infinitely deep would take all
of the memory that is available yet specifies an infinite amount of memory.

>> I am trying to validate whether or not my Prolog code encodes the Liar
>> Paradox.
>
> That cannot be inferred from Prolog rules. Prolog defines some encodings
> like how to encode numbers with characters of Prolog character set but for
> more complex things you must make your own encoding rules.
>
> Mikko
>

This says that G is logically equivalent to its own unprovability in F
G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<IWtbK.40171$JaS8.23866@fx47.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8524&group=comp.ai.philosophy#8524

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!npeer.as286.net!npeer-ng0.as286.net!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx47.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<t4ljjp$4ph$1@dont-email.me> <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 52
Message-ID: <IWtbK.40171$JaS8.23866@fx47.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sun, 1 May 2022 07:12:41 -0400
X-Received-Bytes: 3218
 by: Richard Damon - Sun, 1 May 2022 11:12 UTC

On 5/1/22 6:58 AM, olcott wrote:
> On 5/1/2022 4:24 AM, Mikko wrote:
>> On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:
>>
>>> I just want to add some small note.
>>>
>>> This "not(true(_))" thing is misleading.
>>> Please note that it is *not* a negation.
>>> Functionally it is equivalent to:
>>>
>>> X = foo(bar(X)).
>>
>> That's correct. Prolog language does not give any inherent semantics to
>> data structures. It only defines the execution semantics of language
>> structures and standard library symbols. Those same synbols can be used
>> in data structures with entirely different purposes.
>>
>> Mikko
>>
>
> negation, not, \+
> The concept of logical negation in Prolog is problematical, in the sense
> that the only method that Prolog can use to tell if a proposition is
> false is to try to prove it (from the facts and rules that it has been
> told about), and then if this attempt fails, it concludes that the
> proposition is false. This is referred to as negation as failure.
>
> http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
> This is actually a superior model to convention logic in that it only
> seeks to prove not true, thus detects expressions of language that are
> simply not truth bearers.
>
>
> Expressions of (formal or natural) language that can possibly be
> resolved to a truth value are [truth bearers].
>
> There are only two ways that an expression of language can be resolved
> to a truth value:
> (1) An expression of language is assigned a truth value such as "cats
> are animals" is defined to be true.
>
> (2) Truth preserving operations are applied to expressions of language
> that are known to be true. {cats are animals} and {animals are living
> things} therefore {cats are living things}. Copyright 2021 PL Olcott
>
>

So you are sort of answering your own question. The model of logic that
Prolog handles isn't quite the same as "conventional" logic, in part due
to the way it (doesn't) define Logical Negation.

This seems to fit into your standard misunderstanding of things.

Re: Is this correct Prolog?

<10ubK.688746$LN2.71023@fx13.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8525&group=comp.ai.philosophy#8525

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!2.eu.feeder.erje.net!feeder.erje.net!feeder1.feed.usenet.farm!feed.usenet.farm!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx13.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 119
Message-ID: <10ubK.688746$LN2.71023@fx13.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sun, 1 May 2022 07:18:22 -0400
X-Received-Bytes: 6432
 by: Richard Damon - Sun, 1 May 2022 11:18 UTC

On 4/30/22 11:15 PM, olcott wrote:
> On 4/30/2022 10:11 PM, Richard Damon wrote:
>> On 4/30/22 10:56 PM, olcott wrote:
>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>
>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>
>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>> false.
>>>>>>>>>
>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>
>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>> is correct.
>>>>>>>>
>>>>>>>> All that false means is that the statement
>>>>>>>>
>>>>>>>>
>>>>>>>> LP = not(true(LP))
>>>>>>>>
>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>> its limited logic rules.
>>>>>>>>
>>>>>>>
>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>> nested definition like this:
>>>>>>
>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>
>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>
>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>> can't handle many higher order logical structures.
>>>>>>
>>>>>> Note, for instance, at least some ways of writing factorial for an
>>>>>> unknown value can lead to an infinite expansion, but the factorial
>>>>>> is well defined for all positive integers. The fact that a "prolog
>>>>>> like" expansion operator might not be able to handle the
>>>>>> definition, doesn't mean it doesn't have meaning.
>>>>>>
>>>>>
>>>>> It is really dumb that you continue to take wild guesses again the
>>>>> verified facts.
>>>>>
>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text and
>>>>> eliminate your ignorance.
>>>>>
>>>>
>>>> I did. You just don't seem to understand what I am saying because it
>>>> is above your head.
>>>>
>>>> Prolog is NOT the defining authority for what is a valid logical
>>>> statement, but a system of programming to handle a subset of those
>>>> statements (a useful subset, but a subset).
>>>>
>>>> The fact that Prolog doesn't allow something doesn't mean it doesn't
>>>> have a logical meaning, only that it doesn't have a logical meaning
>>>> in Prolog.
>>> In this case it does. I have spent thousands of hours on the semantic
>>> error of infinitely recursive definition and written a dozen papers
>>> on it. Glancing at one of two of the words of Clocksin & Mellish does
>>> not count as reading it.
>>
>> And it appears that you don't understand it, because you still make
>> category errors when trying to talk about it.
>>
>>>
>>> BEGIN:(Clocksin & Mellish 2003:254)
>>> Finally, a note about how Prolog matching sometimes differs from the
>>> unification used in Resolution. Most Prolog systems will allow you to
>>> satisfy goals like:
>>>
>>>    equal(X, X).?-
>>>    equal(foo(Y), Y).
>>>
>>> that is, they will allow you to match a term against an
>>> uninstantiated subterm of itself. In this example, foo(Y) is matched
>>> against Y, which appears within it. As a result, Y will stand for
>>> foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is
>>> foo(foo(foo(Y))), and so on. So Y ends up standing for some kind of
>>> infinite structure.
>>> END:(Clocksin & Mellish 2003:254)
>>>
>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>
>>
>> Right. but some infinite structures might actually have meaning.
> Not in this case, it is very obvious that no theorem prover can possibly
> prove any infinite expression. It is the same thing as a program that is
> stuck in an infinite loop.
>

As Jeff pointed out, your claim is shown false, that some statements
with infinite expansions can be worked with by some automatic solvers.
This just proves that you don't really understand the effects of
"recursion" and "self-reference", and perhaps a source of your error in
trying to reason about thing like this Halting Problem proof or Godels
Incompleteness Theory and his expression "G".

If something that is obviously undoable is your mind is shown to be in
fact doable, the problem isn't in the ability to do it, but in the
ability of your mind to understand. Your misconceptions don't change the
nature of reality, but reality proves you wrong.

Re: Is this correct Prolog?

<u7ubK.20174$HLy4.14606@fx38.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8526&group=comp.ai.philosophy#8526

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!npeer.as286.net!npeer-ng0.as286.net!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx38.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me> <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 70
Message-ID: <u7ubK.20174$HLy4.14606@fx38.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sun, 1 May 2022 07:26:18 -0400
X-Received-Bytes: 3486
 by: Richard Damon - Sun, 1 May 2022 11:26 UTC

On 5/1/22 7:06 AM, olcott wrote:
> On 5/1/2022 4:38 AM, Mikko wrote:
>> On 2022-04-30 20:48:47 +0000, olcott said:
>>
>>> On 4/30/2022 4:31 AM, Mikko wrote:
>>>> On 2022-04-30 07:02:23 +0000, olcott said:
>>>>
>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>
>>>>> ?- LP = not(true(LP)).
>>>>> LP = not(true(LP)).
>>>>
>>>> This is correct but to fail would also be correct.
>>>>
>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>> false.
>>>>
>>>> unify_with_occurs_check must fail if the unified data structure
>>>> would contain loops.
>>>>
>>>> Mikko
>>>>
>>>
>>> The above is the actual execution of actual Prolog code using
>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4).
>>
>> Another Prolog implementation might interprete LP = not(true(LP))
>> differently
>> and still conform to the prolog standard.
>>
>>> According to Clocksin & Mellish it is not a mere loop, it is an
>>> "infinite term" thus infinitely recursive definition.
>>
>> When discussing data structures, "infinite" and "loop" mean the same.
>> The data structure is infinitely deep but contains only finitely many
>> distinct objects and occupies only a finite amount of memory.
>>
>
> That is incorrect. any structure that is infinitely deep would take all
> of the memory that is available yet specifies an infinite amount of memory.

Nope, a tree that one branch points into itself higher up represents a
tree with infinite depth, but only needs a finite amount of memory.
Building such a structure may require the ability to forward declare
something or reference something not yet defined.

Some infinities have finite representation. You don't seem able to
understand that.

Yes, some naive ways of expanding them fail, but the answer to that is
you just don't do that, but need to use a less naive method.

>
>>> I am trying to validate whether or not my Prolog code encodes the
>>> Liar Paradox.
>>
>> That cannot be inferred from Prolog rules. Prolog defines some encodings
>> like how to encode numbers with characters of Prolog character set but
>> for
>> more complex things you must make your own encoding rules.
>>
>> Mikko
>>
>
> This says that G is logically equivalent to its own unprovability in F
> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.
>
>

Re: Is this correct Prolog?

<EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8527&group=comp.ai.philosophy#8527

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!1.us.feeder.erje.net!feeder.erje.net!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:28:29 -0500
Date: Sun, 1 May 2022 06:28:28 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4lkro$dl6$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4lkro$dl6$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 64
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-Mknwy0jR7Vdu50vSGP1AIXQHj7Tu8Pu+tNjuX2UvBOOINhboy8p/oOXG2OKH6nCgjOSsEkFFvws/tFb!DCvVLGo3EBk4HfkXlbC/woN13JIs05P+Yy/QkabD1i1JPvJXNhS+qTJYrqIHnYlAh4smck4QsLo=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4358
 by: olcott - Sun, 1 May 2022 11:28 UTC

On 5/1/2022 4:45 AM, Mikko wrote:
> On 2022-05-01 03:15:56 +0000, olcott said:
>
>> Not in this case, it is very obvious that no theorem prover can
>> possibly prove any infinite expression.
>
> Doesn't matter as you can't give an infinite expression to a theorem
> prover.
>
> Mikko
>

*You can and Prolog can detect and reject it*

BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:

equal(X, X).?-
equal(foo(Y), Y).

that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.

<inserted for clarity>
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
</inserted for clarity>

Note that, whereas they may allow you to construct something like this,
most Prolog systems will not be able to write it out at the end.
According to the formal definition of Unification, this kind of
“infinite term” should never come to exist. Thus Prolog systems that
allow a term to match an uninstantiated subterm of itself do not act
correctly as Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be instantiated to
something containing itself. Such a check, an occurs check, would be
straightforward to implement, but would slow down the execution of
Prolog programs considerably. Since it would only affect very few
programs, most implementors have simply left it out 1.

1 The Prolog standard states that the result is undefined if a Prolog
system attempts to match a term against an uninstantiated subterm of
itself, which means that programs which cause this to happen will not
be portable. A portable program should ensure that wherever an occurs
check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an occurs
check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)

Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the
ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<_v2dnUiL-Yjh7fP_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8528&group=comp.ai.philosophy#8528

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:35:24 -0500
Date: Sun, 1 May 2022 06:35:23 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4l5hq$8bi$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4l5hq$8bi$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <_v2dnUiL-Yjh7fP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 206
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-3Vn6S2Q4oDLUo5OfIP0/LhyiWpZ3GSFYvQ4GqImO21AW31aziES/M/D1m1gdRP3CETSo1tGY/il6KT9!SWRfef90NXFGS/FE7x2fHUpUl+SggdQsnb+DsUtVV/4IvS7YwUGalPHxpT5c8bPTTth4o9aFmqI=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 10912
 by: olcott - Sun, 1 May 2022 11:35 UTC

On 5/1/2022 12:24 AM, Jeff Barnett wrote:
> On 4/30/2022 9:15 PM, olcott wrote:
>> On 4/30/2022 10:11 PM, Richard Damon wrote:
>>> On 4/30/22 10:56 PM, olcott wrote:
>>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>>
>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>
>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>> false.
>>>>>>>>>>
>>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>>
>>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>>> is correct.
>>>>>>>>>
>>>>>>>>> All that false means is that the statement
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> LP = not(true(LP))
>>>>>>>>>
>>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>>> its limited logic rules.
>>>>>>>>>
>>>>>>>>
>>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>>> nested definition like this:
>>>>>>>
>>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>>
>>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>>
>>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>>> can't handle many higher order logical structures.
>>>>>>>
>>>>>>> Note, for instance, at least some ways of writing factorial for
>>>>>>> an unknown value can lead to an infinite expansion, but the
>>>>>>> factorial is well defined for all positive integers. The fact
>>>>>>> that a "prolog like" expansion operator might not be able to
>>>>>>> handle the definition, doesn't mean it doesn't have meaning.
>>>>>>>
>>>>>>
>>>>>> It is really dumb that you continue to take wild guesses again the
>>>>>> verified facts.
>>>>>>
>>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text
>>>>>> and eliminate your ignorance.
>>>>>>
>>>>>
>>>>> I did. You just don't seem to understand what I am saying because
>>>>> it is above your head.
>>>>>
>>>>> Prolog is NOT the defining authority for what is a valid logical
>>>>> statement, but a system of programming to handle a subset of those
>>>>> statements (a useful subset, but a subset).
>>>>>
>>>>> The fact that Prolog doesn't allow something doesn't mean it
>>>>> doesn't have a logical meaning, only that it doesn't have a logical
>>>>> meaning in Prolog.
>>>> In this case it does. I have spent thousands of hours on the
>>>> semantic error of infinitely recursive definition and written a
>>>> dozen papers on it. Glancing at one of two of the words of Clocksin
>>>> & Mellish does not count as reading it.
>>>
>>> And it appears that you don't understand it, because you still make
>>> category errors when trying to talk about it.
>>>
>>>>
>>>> BEGIN:(Clocksin & Mellish 2003:254)
>>>> Finally, a note about how Prolog matching sometimes differs from the
>>>> unification used in Resolution. Most Prolog systems will allow you
>>>> to satisfy goals like:
>>>>
>>>>    equal(X, X).?-
>>>>    equal(foo(Y), Y).
>>>>
>>>> that is, they will allow you to match a term against an
>>>> uninstantiated subterm of itself. In this example, foo(Y) is matched
>>>> against Y, which appears within it. As a result, Y will stand for
>>>> foo(Y), which is foo(foo(Y)) (because of what Y stands for), which
>>>> is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind
>>>> of infinite structure.
>>>> END:(Clocksin & Mellish 2003:254)
>>>>
>>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>>
>>>
>>> Right. but some infinite structures might actually have meaning.
>> Not in this case, it is very obvious that no theorem prover can
>> possibly prove any infinite expression. It is the same thing as a
>> program that is stuck in an infinite loop.
>
> Richard wrote and the asshole (PO) snipped
> ------------------------------------------
> Right. but some infinite structures might actually have meaning. The
> fact that Prolog uses certain limited method to figure out meaning
> doesn't mean that other methods can't find the meaning.
>

The question is not whether some infinite structures have meaning that
is the dishonest dodge of the strawman error.

The question is whether on not the expression at hand has meaning or is
simply semantically incoherent. I just posted all of the Clocksin &
Mellish text in my prior post to make this more clear.

This example expanded from Clocksin & Mellish conclusively proves that
some expressions of language are incorrect:

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))

> Just like:
>
> Fact(n) := (N == 1) ? 1 : N*Fact(n-1);
>
> if naively expanded has an infinite expansion.
>
> But, based on mathematical knowledge, and can actually be proven from
> the definition, something like Fact(n+1)/fact(n), even for an unknown n,
> can be reduced without the need to actually expend infinite operations.
>
> Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't
> abort its simulation, then for THAT H^, we have that H^(H^) is
> non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a
> counter example
>
> When you program H to abort its simulation of H^ at some point, and
> build your H^ on that H, then H(H^,H^), will return the non-halting
> answer, and H^(H^) when PROPERLY run or simulated halts, because H has
> the same "cut off" logic at the factorial above.
>
> The naive expansion thinks it is infinite, but the correct expansion
> sees the cut off and sees that it is actually finite.
> ----------------------------------------------------------------------
>
> A good symbolic manipulation system or a theorem prover with appropriate
> axioms and rules of inference could surely handle forms such as
> Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant
> fool, who seems to think that the unthinking infinite unrolling of a
> form must occur. Only you would think that a solver system would
> completely unroll a form before analyzing it and applying
> transformations to it.
>
> Son, it don't work that way (unless you are defining and making a mess
> trying to write the system yourself). Systems usually have rules that
> make small incremental transformations and usually search breadth first
> with perhaps a limited amount of depth first interludes. If they don't
> use a breadth first strategy, they will not be able to claim the
> completeness property. (See resolution theorem prover literature for
> some explanation. You wont understand it but you can cite as if you did!)
>
> Richard was trying to explain this to you in the snipped portion I
> recited just above. Question for Peter holding his pecker: How do you
> always and I mean always manage to delete the part of a message you
> respond too that addresses the point you now try to make?
>
> A typically subsequence you might see in the trace: would include in
> order but not necessarily consecutively:
>    Fact(n+1)/Fact(n)
>    (n+1)*Fact(n)/Fact(n)
>    (n+1)
> Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found
> too. In some circumstances, these other terms might be helpful. A
> theorem prover or manipulator does all of this, breadth first, hoping to
> blindly stumble on a solution. You can provide heuristics that might
> speed up the process but no advice short of an oracle will get you even
> one more result. (Another manifestation of HP.) It's the slow grinding
> through the possibilities that guarantees that if a result can be found,
> it will be found. And all the theory that you don't understand says
> that's the best you can do.
>
> Ben and I disagree on reasons for your type of total dishonesty. He
> thinks that you are so self deluded that you actual believe what you are
> saying; that you are so self deluded that the dishonest utterances are
> just your subconscious protecting your already damaged ego. To that, I
> say phooey; you are just a long term troll who lies a lot about math,
> about your history and health, and about your accomplishments.
>
> I don't believe that you will read this before you start to respond but
> that's okay. Understanding is not required. Neither is respect in either
> direction.


Click here to read the complete article
Re: Is this correct Prolog?

<lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8530&group=comp.ai.philosophy#8530

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:45:12 -0500
Date: Sun, 1 May 2022 06:45:11 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<t4ljjp$4ph$1@dont-email.me> <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
<IWtbK.40171$JaS8.23866@fx47.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <IWtbK.40171$JaS8.23866@fx47.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 64
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-ncgSsjRowQAjYHPOxhy4/WxmHkobARxXPhBWanvMz0LvL5gjIyT42WtToQG9LrBl8MSrHm9fZfnkMwr!F5blKwYvUeJVrI7B0B93ayX8/VWIHZYP3RT7lA4CybN5GxDEshyI9a5WyvJGC3NuPhCZKBivqQ8=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3896
 by: olcott - Sun, 1 May 2022 11:45 UTC

On 5/1/2022 6:12 AM, Richard Damon wrote:
> On 5/1/22 6:58 AM, olcott wrote:
>> On 5/1/2022 4:24 AM, Mikko wrote:
>>> On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:
>>>
>>>> I just want to add some small note.
>>>>
>>>> This "not(true(_))" thing is misleading.
>>>> Please note that it is *not* a negation.
>>>> Functionally it is equivalent to:
>>>>
>>>> X = foo(bar(X)).
>>>
>>> That's correct. Prolog language does not give any inherent semantics to
>>> data structures. It only defines the execution semantics of language
>>> structures and standard library symbols. Those same synbols can be used
>>> in data structures with entirely different purposes.
>>>
>>> Mikko
>>>
>>
>> negation, not, \+
>> The concept of logical negation in Prolog is problematical, in the
>> sense that the only method that Prolog can use to tell if a
>> proposition is false is to try to prove it (from the facts and rules
>> that it has been told about), and then if this attempt fails, it
>> concludes that the proposition is false. This is referred to as
>> negation as failure.
>>
>> http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
>> This is actually a superior model to convention logic in that it only
>> seeks to prove not true, thus detects expressions of language that are
>> simply not truth bearers.
>>
>>
>> Expressions of (formal or natural) language that can possibly be
>> resolved to a truth value are [truth bearers].
>>
>> There are only two ways that an expression of language can be resolved
>> to a truth value:
>> (1) An expression of language is assigned a truth value such as "cats
>> are animals" is defined to be true.
>>
>> (2) Truth preserving operations are applied to expressions of language
>> that are known to be true. {cats are animals} and {animals are living
>> things} therefore {cats are living things}. Copyright 2021 PL Olcott
>>
>>
>
> So you are sort of answering your own question. The model of logic that
> Prolog handles isn't quite the same as "conventional" logic, in part due
> to the way it (doesn't) define Logical Negation.
>
> This seems to fit into your standard misunderstanding of things.

Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<npSdnachY_1p7vP_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8531&group=comp.ai.philosophy#8531

 copy link   Newsgroups: comp.theory comp.ai.philosophy comp.lang.prolog
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:50:12 -0500
Date: Sun, 1 May 2022 06:50:11 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
<10ubK.688746$LN2.71023@fx13.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <10ubK.688746$LN2.71023@fx13.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <npSdnachY_1p7vP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 138
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-hY8z0tIEjT2/HN2i1vbJvjw8orzDBVo2fCePnkOGm8U+67Z0WD3motgW9JGZ4Bb4DjgZbZUzflUx/PJ!Lh3RH28RgFLPukcsGSSnxICcrLpD8PDc9N08eNU2P/GeXxkbN1f521WXV+CYdaC1+up/LZUTgh0=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 7389
 by: olcott - Sun, 1 May 2022 11:50 UTC

On 5/1/2022 6:18 AM, Richard Damon wrote:
> On 4/30/22 11:15 PM, olcott wrote:
>> On 4/30/2022 10:11 PM, Richard Damon wrote:
>>> On 4/30/22 10:56 PM, olcott wrote:
>>>> On 4/30/2022 9:38 PM, Richard Damon wrote:
>>>>> On 4/30/22 10:21 PM, olcott wrote:
>>>>>> On 4/30/2022 9:00 PM, Richard Damon wrote:
>>>>>>> On 4/30/22 9:42 PM, olcott wrote:
>>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>>
>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>
>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>> false.
>>>>>>>>>>
>>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>>
>>>>>>>>>> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>>> is correct.
>>>>>>>>>
>>>>>>>>> All that false means is that the statement
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> LP = not(true(LP))
>>>>>>>>>
>>>>>>>>> is recursive and that Prolog can't actually evaluate it due to
>>>>>>>>> its limited logic rules.
>>>>>>>>>
>>>>>>>>
>>>>>>>> That is not what Clocksin & Mellish says. They say it is an
>>>>>>>> erroneous "infinite term" meaning that it specifies infinitely
>>>>>>>> nested definition like this:
>>>>>>>
>>>>>>> No, that IS what they say, that this sort of recursion fails the
>>>>>>> test of Unification, not that it is has no possible logical meaning.
>>>>>>>
>>>>>>> Prolog represents a somewhat basic form of logic, useful for many
>>>>>>> cases, but not encompassing all possible reasoning systems.
>>>>>>>
>>>>>>> Maybe it can handle every one that YOU can understand, but it
>>>>>>> can't handle many higher order logical structures.
>>>>>>>
>>>>>>> Note, for instance, at least some ways of writing factorial for
>>>>>>> an unknown value can lead to an infinite expansion, but the
>>>>>>> factorial is well defined for all positive integers. The fact
>>>>>>> that a "prolog like" expansion operator might not be able to
>>>>>>> handle the definition, doesn't mean it doesn't have meaning.
>>>>>>>
>>>>>>
>>>>>> It is really dumb that you continue to take wild guesses again the
>>>>>> verified facts.
>>>>>>
>>>>>> Please read the Clocksin & Mellish (on page 3 of my paper) text
>>>>>> and eliminate your ignorance.
>>>>>>
>>>>>
>>>>> I did. You just don't seem to understand what I am saying because
>>>>> it is above your head.
>>>>>
>>>>> Prolog is NOT the defining authority for what is a valid logical
>>>>> statement, but a system of programming to handle a subset of those
>>>>> statements (a useful subset, but a subset).
>>>>>
>>>>> The fact that Prolog doesn't allow something doesn't mean it
>>>>> doesn't have a logical meaning, only that it doesn't have a logical
>>>>> meaning in Prolog.
>>>> In this case it does. I have spent thousands of hours on the
>>>> semantic error of infinitely recursive definition and written a
>>>> dozen papers on it. Glancing at one of two of the words of Clocksin
>>>> & Mellish does not count as reading it.
>>>
>>> And it appears that you don't understand it, because you still make
>>> category errors when trying to talk about it.
>>>
>>>>
>>>> BEGIN:(Clocksin & Mellish 2003:254)
>>>> Finally, a note about how Prolog matching sometimes differs from the
>>>> unification used in Resolution. Most Prolog systems will allow you
>>>> to satisfy goals like:
>>>>
>>>>    equal(X, X).?-
>>>>    equal(foo(Y), Y).
>>>>
>>>> that is, they will allow you to match a term against an
>>>> uninstantiated subterm of itself. In this example, foo(Y) is matched
>>>> against Y, which appears within it. As a result, Y will stand for
>>>> foo(Y), which is foo(foo(Y)) (because of what Y stands for), which
>>>> is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind
>>>> of infinite structure.
>>>> END:(Clocksin & Mellish 2003:254)
>>>>
>>>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
>>>>
>>>
>>> Right. but some infinite structures might actually have meaning.
>> Not in this case, it is very obvious that no theorem prover can
>> possibly prove any infinite expression. It is the same thing as a
>> program that is stuck in an infinite loop.
>>
>
> As Jeff pointed out, your claim is shown false, that some statements
> with infinite expansions can be worked with by some automatic solvers.

That is the dishonest dodge of the strawman error. The particular
expression at hand is inherently incorrect and thus any system that
proves it is a broken system.

> This just proves that you don't really understand the effects of
> "recursion" and "self-reference", and perhaps a source of your error in
> trying to reason about thing like this Halting Problem proof or Godels
> Incompleteness Theory and his expression "G".
>

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
The "..." indicates infinite expansion, thus this expression can never
be proved by any system.

> If something that is obviously undoable is your mind is shown to be in
> fact doable, the problem isn't in the ability to do it, but in the
> ability of your mind to understand. Your misconceptions don't change the
> nature of reality, but reality proves you wrong.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8532&group=comp.ai.philosophy#8532

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 06:54:29 -0500
Date: Sun, 1 May 2022 06:54:28 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me> <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
<u7ubK.20174$HLy4.14606@fx38.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <u7ubK.20174$HLy4.14606@fx38.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 88
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-LFvAurXSuuLYhvV6qWSvY32+jLfpk2/AWDD/HyBkVONzozXaK69Q5xj9lA3H4lkhwntd30bfTOJOyCz!wKRcV2mOlT5NTrQalFZ/uhYD7URUuyqDa1Sur7FLV+PywX44ShrpI1aRgOwy3xgQ6aWDJ3PZmeA=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4324
 by: olcott - Sun, 1 May 2022 11:54 UTC

On 5/1/2022 6:26 AM, Richard Damon wrote:
> On 5/1/22 7:06 AM, olcott wrote:
>> On 5/1/2022 4:38 AM, Mikko wrote:
>>> On 2022-04-30 20:48:47 +0000, olcott said:
>>>
>>>> On 4/30/2022 4:31 AM, Mikko wrote:
>>>>> On 2022-04-30 07:02:23 +0000, olcott said:
>>>>>
>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>
>>>>>> ?- LP = not(true(LP)).
>>>>>> LP = not(true(LP)).
>>>>>
>>>>> This is correct but to fail would also be correct.
>>>>>
>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>> false.
>>>>>
>>>>> unify_with_occurs_check must fail if the unified data structure
>>>>> would contain loops.
>>>>>
>>>>> Mikko
>>>>>
>>>>
>>>> The above is the actual execution of actual Prolog code using
>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4).
>>>
>>> Another Prolog implementation might interprete LP = not(true(LP))
>>> differently
>>> and still conform to the prolog standard.
>>>
>>>> According to Clocksin & Mellish it is not a mere loop, it is an
>>>> "infinite term" thus infinitely recursive definition.
>>>
>>> When discussing data structures, "infinite" and "loop" mean the same.
>>> The data structure is infinitely deep but contains only finitely many
>>> distinct objects and occupies only a finite amount of memory.
>>>
>>
>> That is incorrect. any structure that is infinitely deep would take
>> all of the memory that is available yet specifies an infinite amount
>> of memory.
>
> Nope, a tree that one branch points into itself higher up represents a
> tree with infinite depth, but only needs a finite amount of memory.
> Building such a structure may require the ability to forward declare
> something or reference something not yet defined.
>

That is counter-factual. unify_with_occurs_check determines that it
would require infinite memory and then aborts its evaluation.

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
"..." indicates infinite depth, thus infinite string length.

> Some infinities have finite representation. You don't seem able to
> understand that.
>
> Yes, some naive ways of expanding them fail, but the answer to that is
> you just don't do that, but need to use a less naive method.
>

>
>>
>>>> I am trying to validate whether or not my Prolog code encodes the
>>>> Liar Paradox.
>>>
>>> That cannot be inferred from Prolog rules. Prolog defines some encodings
>>> like how to encode numbers with characters of Prolog character set
>>> but for
>>> more complex things you must make your own encoding rules.
>>>
>>> Mikko
>>>
>>
>> This says that G is logically equivalent to its own unprovability in F
>> G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.
>>
>>
>

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

Re: Is this correct Prolog?

<3EubK.14817$6j9b.13866@fx36.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8533&group=comp.ai.philosophy#8533

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!news.swapon.de!fu-berlin.de!bolzen.all.de!npeer.as286.net!npeer-ng0.as286.net!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx36.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4lkro$dl6$1@dont-email.me>
<EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 71
Message-ID: <3EubK.14817$6j9b.13866@fx36.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sun, 1 May 2022 08:01:05 -0400
X-Received-Bytes: 4562
 by: Richard Damon - Sun, 1 May 2022 12:01 UTC

On 5/1/22 7:28 AM, olcott wrote:
> On 5/1/2022 4:45 AM, Mikko wrote:
>> On 2022-05-01 03:15:56 +0000, olcott said:
>>
>>> Not in this case, it is very obvious that no theorem prover can
>>> possibly prove any infinite expression.
>>
>> Doesn't matter as you can't give an infinite expression to a theorem
>> prover.
>>
>> Mikko
>>
>
> *You can and Prolog can detect and reject it*

Which just shows PROLOG can't handle that sort of expression, not that
it logically doens't have a meaning.

>
> BEGIN:(Clocksin & Mellish 2003:254)
> Finally, a note about how Prolog matching sometimes differs from the
> unification used in Resolution. Most Prolog systems will allow you to
> satisfy goals like:
>
>   equal(X, X).?-
>   equal(foo(Y), Y).
>
> that is, they will allow you to match a term against an uninstantiated
> subterm of itself. In this example, foo(Y) is matched against Y, which
> appears within it. As a result, Y will stand for foo(Y), which is
> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
> and so on. So Y ends up standing for some kind of infinite structure.
>
> <inserted for clarity>
> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
> </inserted for clarity>
>
> Note that, whereas they may allow you to construct something like this,
> most Prolog systems will not be able to write it out at the end.
> According to the formal definition of Unification, this kind of
> “infinite term” should never come to exist. Thus Prolog systems that
> allow a term to match an uninstantiated subterm of itself do not act
> correctly as Resolution theorem provers. In order to make them do so, we
> would have to add a check that a variable cannot be instantiated to
> something containing itself. Such a check, an occurs check, would be
> straightforward to implement, but would slow down the execution of
> Prolog programs considerably. Since it would only affect very few
> programs, most implementors have simply left it out 1.
>
> 1 The Prolog standard states that the result is undefined if a Prolog
> system attempts to match a term against an uninstantiated subterm of
> itself, which means that programs which cause this  to happen will not
> be portable. A portable program should ensure that wherever an occurs
> check might be applicable the built-in predicate
> unify_with_occurs_check/2 is used explicitly instead of the normal
> unification operation of the Prolog implementation. As its name
> suggests, this predicate acts like =/2 except that it fails if an occurs
> check detects an illegal attempt to instantiate a variable.
> END:(Clocksin & Mellish 2003:254)
>
> Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the
> ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
>

So all Clocksin & Melish is saying is that such an expression fails in
PROLOG, not that it doesn't have a valid logical meaning.

The world is NOT Prolog, and I suspect Prolog isn't sufficient to handle
the logic needed to process the Godel Sentence, so can't be used to
disprove it.

Re: Is this correct Prolog?

<SJubK.452730$iK66.338793@fx46.iad>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8534&group=comp.ai.philosophy#8534

 copy link   Newsgroups: comp.lang.prolog comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!feeder1.feed.usenet.farm!feed.usenet.farm!peer01.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx46.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<t4ljjp$4ph$1@dont-email.me> <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
<IWtbK.40171$JaS8.23866@fx47.iad>
<lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 70
Message-ID: <SJubK.452730$iK66.338793@fx46.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sun, 1 May 2022 08:07:14 -0400
X-Received-Bytes: 4143
 by: Richard Damon - Sun, 1 May 2022 12:07 UTC

On 5/1/22 7:45 AM, olcott wrote:
> On 5/1/2022 6:12 AM, Richard Damon wrote:
>> On 5/1/22 6:58 AM, olcott wrote:
>>> On 5/1/2022 4:24 AM, Mikko wrote:
>>>> On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:
>>>>
>>>>> I just want to add some small note.
>>>>>
>>>>> This "not(true(_))" thing is misleading.
>>>>> Please note that it is *not* a negation.
>>>>> Functionally it is equivalent to:
>>>>>
>>>>> X = foo(bar(X)).
>>>>
>>>> That's correct. Prolog language does not give any inherent semantics to
>>>> data structures. It only defines the execution semantics of language
>>>> structures and standard library symbols. Those same synbols can be used
>>>> in data structures with entirely different purposes.
>>>>
>>>> Mikko
>>>>
>>>
>>> negation, not, \+
>>> The concept of logical negation in Prolog is problematical, in the
>>> sense that the only method that Prolog can use to tell if a
>>> proposition is false is to try to prove it (from the facts and rules
>>> that it has been told about), and then if this attempt fails, it
>>> concludes that the proposition is false. This is referred to as
>>> negation as failure.
>>>
>>> http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
>>> This is actually a superior model to convention logic in that it only
>>> seeks to prove not true, thus detects expressions of language that
>>> are simply not truth bearers.
>>>
>>>
>>> Expressions of (formal or natural) language that can possibly be
>>> resolved to a truth value are [truth bearers].
>>>
>>> There are only two ways that an expression of language can be
>>> resolved to a truth value:
>>> (1) An expression of language is assigned a truth value such as "cats
>>> are animals" is defined to be true.
>>>
>>> (2) Truth preserving operations are applied to expressions of
>>> language that are known to be true. {cats are animals} and {animals
>>> are living things} therefore {cats are living things}. Copyright 2021
>>> PL Olcott
>>>
>>>
>>
>> So you are sort of answering your own question. The model of logic
>> that Prolog handles isn't quite the same as "conventional" logic, in
>> part due to the way it (doesn't) define Logical Negation.
>>
>> This seems to fit into your standard misunderstanding of things.
>
> Prolog has a better model in that it can detect semantic paradoxes.
> LP ↔ ¬True(LP) is correctly assessed as neither true nor false.
>

"Better" is as subjective word unless you define an objective criteria.
The fact that Prolog doesn't have the expresiability to actually write
the Godel sentence, means it can't actually be used to disprove it.

Misusing notations to show something is invalid logic.

I don't know Prolog well enough, but if the statement doesn't actaully
mean what you want it to mean to Prolog (as others have said), then the
fact that Prolog gives you the answer you want doesn't mean anything.

Pages:123456
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor