On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
> On 5/2/22 18:04, olcott wrote:
>
> > Is there any Prolog that can detect that the above will not terminate
> > prior to executing it?
>
> As I have said previously, my example is naïve.

And as I have pointed out to you, your "solution" solves nothing at all.

> Maybe if you will think
> hard enough you can make it detect such conditions, probably by writing
> meta-interpreter of some sort, and terminate. Personally, I don't think
> that using Prolog can be accepted as a "rigorous proof" of anything.

That's just nonsense: Prolog is a formal language no less than any other.
Plus you too must think you have a solution to the halting problem...

Enough said.

Julio

On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE

I will attempt to summarize the level of the idiot's understanding of
Prolog: The level is the same as of his understanding of math, logic, C,
C++, software engineering, programming, programming methodology, Turing
Machines, and other specific topics in these general categories. He is
capable of moving his eyes through a few paragraphs but not reading
anything. This is a common learning disability. He can cut and paste
from what little is eyes scan but, in general, he can neither comprehend
the little he's seen nor can he amalgamate concepts from the bits and
pieces he has visited.

His approach to gaining and demonstrating understanding is best
represented by a comic's view of monkeys exploring objects new to them:
biting things, hitting other objects with the new one, stirring feces
and seeing if it will stick and can be thrown etc. The problem with this
metaphor is that monkeys are intelligent and our idiot is not. When the
monkey is done with initial exploration, it has an idea whether the new
object can serve some useful purpose; in any event, the monkey had fun.
The idiot, on the other hand, never discoveries the usefulness of the
potential new knowledge because he doesn't have the attention span or
curiosity to do so. That's why he is an idiot and not as smart or as
wise as the monkey though he too has fun.
--
Jeff Barnett

On 5/2/22 18:51, Julio Di Egidio wrote:
> On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
>> On 5/2/22 18:04, olcott wrote:
>>
>>> Is there any Prolog that can detect that the above will not terminate
>>> prior to executing it?
>>
>> As I have said previously, my example is naïve.
>
> And as I have pointed out to you, your "solution" solves nothing at all.

The request from topic poster was — how would I represent sentence "This
sentence is not provable". I came up with some small example of "not
provable sentence" which happens to be a simple infinite loop. I did
*not* claim that it captures anything deep and solves halting problem,
that would've been absurd. If you have any better idea please write it.

>> Maybe if you will think
>> hard enough you can make it detect such conditions, probably by writing
>> meta-interpreter of some sort, and terminate. Personally, I don't think
>> that using Prolog can be accepted as a "rigorous proof" of anything.
>
> That's just nonsense: Prolog is a formal language no less than any other.
> Plus you too must think you have a solution to the halting problem...

No, I don't have a solution for a halting problem, I'm not a freak, but
also solving termination for _some_ specially designed simple programs
doesn't require halting problem. It's some first grader stuff, c'mon.

Like this random example from my head (in C++):

int sum = 0;
for (int i = 5; i > 0; i--)
sum += i;

Can be proved to always terminate, because loop's variant `i` has lower
bound, has total ordering and it's value decreases on each iteration. In
some cases you can automatically detect such loop variants, and
automatically prove termination of _some_ loops.

--
Alex Grabowski

On Monday, 2 May 2022 at 19:39:01 UTC+2, Aleksy Grabowski wrote:
> On 5/2/22 18:51, Julio Di Egidio wrote:
> > On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
> >> On 5/2/22 18:04, olcott wrote:
> >>
> >>> Is there any Prolog that can detect that the above will not terminate
> >>> prior to executing it?
> >>
> >> As I have said previously, my example is naïve.
> >
> > And as I have pointed out to you, your "solution" solves nothing at all..
> The request from topic poster was — how would I represent sentence "This
> sentence is not provable". I came up with some small example

No, you didn't, and I have said why twice by now.

> >> Maybe if you will think
> >> hard enough you can make it detect such conditions, probably by writing
> >> meta-interpreter of some sort, and terminate. Personally, I don't think
> >> that using Prolog can be accepted as a "rigorous proof" of anything.
> >
> > That's just nonsense: Prolog is a formal language no less than any other.
> > Plus you too must think you have a solution to the halting problem...
>
> No, I don't have a solution for a halting problem, I'm not a freak, but
> also solving termination for _some_ specially designed simple programs
> doesn't require halting problem. It's some first grader stuff, c'mon.

You bring it up: and it is in fact irrelevant here, as long as the
original question is the question you noticed it is.

Anyway, discussing with Olcott's interlocutors is always even
worse than discussing with Olcott himself...

(EOD.)

Julio

On Mon, 2 May 2022 11:28:23 -0600
Jeff Barnett <jbb@notatt.com> wrote:

> On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE
>
>
> I will attempt to summarize the level of the idiot's understanding of
> Prolog: The level is the same as of his understanding of math, logic,
> C, C++, software engineering, programming, programming methodology,
> Turing Machines, and other specific topics in these general
> categories. He is capable of moving his eyes through a few paragraphs
> but not reading anything. This is a common learning disability. He
> can cut and paste from what little is eyes scan but, in general, he
> can neither comprehend the little he's seen nor can he amalgamate
> concepts from the bits and pieces he has visited.
>
> His approach to gaining and demonstrating understanding is best
> represented by a comic's view of monkeys exploring objects new to
> them: biting things, hitting other objects with the new one, stirring
> feces and seeing if it will stick and can be thrown etc. The problem
> with this metaphor is that monkeys are intelligent and our idiot is
> not. When the monkey is done with initial exploration, it has an idea
> whether the new object can serve some useful purpose; in any event,
> the monkey had fun. The idiot, on the other hand, never discoveries
> the usefulness of the potential new knowledge because he doesn't have
> the attention span or curiosity to do so. That's why he is an idiot
> and not as smart or as wise as the monkey though he too has fun.

The ad hominem attack is a logical fallacy: so it is in fact YOU who is
throwing excrement at the walls, not Olcott. Attack the argument not the
person, dear.

https://en.wikipedia.org/wiki/Ad_hominem

/Flibble

On 5/2/2022 12:38 PM, Aleksy Grabowski wrote:
> On 5/2/22 18:51, Julio Di Egidio wrote:
>> On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
>>> On 5/2/22 18:04, olcott wrote:
>>>
>>>> Is there any Prolog that can detect that the above will not terminate
>>>> prior to executing it?
>>>
>>> As I have said previously, my example is naïve.
>>
>> And as I have pointed out to you, your "solution" solves nothing at all.
>
> The request from topic poster was — how would I represent sentence "This
> sentence is not provable". I came up with some small example of "not
> provable sentence" which happens to be a simple infinite loop. I did
> *not* claim that it captures anything deep and solves halting problem,
> that would've been absurd. If you have any better idea please write it.
>

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

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

I simplified it because the "not" of Prolog "negation as failure"
already means not(true(LP)) when we assume that true(LP) means
provable(LP).

This version precisely captures the pathological self-reference of the
Liar Paradox in a way that Prolog detects and rejects.

"equal" converted to = for SWI Prolog

?- =(foo(Y), Y).
Y = foo(Y).

?- unify_with_occurs_check(Y, foo(Y)).
false

>>> Maybe if you will think
>>> hard enough you can make it detect such conditions, probably by writing
>>> meta-interpreter of some sort, and terminate. Personally, I don't think
>>> that using Prolog can be accepted as a "rigorous proof" of anything.
>>
>> That's just nonsense: Prolog is a formal language no less than any other.
>> Plus you too must think you have a solution to the halting problem...
>
> No, I don't have a solution for a halting problem, I'm not a freak, but
> also solving termination for _some_ specially designed simple programs
> doesn't require halting problem. It's some first grader stuff, c'mon.
>
> Like this random example from my head (in C++):
>
>     int sum = 0;
>     for (int i = 5; i > 0; i--)
>         sum += i;
>
> Can be proved to always terminate, because loop's variant `i` has lower
> bound, has total ordering and it's value decreases on each iteration. In
> some cases you can automatically detect such loop variants, and
> automatically prove termination of _some_ loops.
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 1:04 PM, Julio Di Egidio wrote:
> On Monday, 2 May 2022 at 19:39:01 UTC+2, Aleksy Grabowski wrote:
>> On 5/2/22 18:51, Julio Di Egidio wrote:
>>> On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
>>>> On 5/2/22 18:04, olcott wrote:
>>>>
>>>>> Is there any Prolog that can detect that the above will not terminate
>>>>> prior to executing it?
>>>>
>>>> As I have said previously, my example is naïve.
>>>
>>> And as I have pointed out to you, your "solution" solves nothing at all.
>> The request from topic poster was — how would I represent sentence "This
>> sentence is not provable". I came up with some small example
>
> No, you didn't, and I have said why twice by now.
>

Encoding "This sentence is not true" in Prolog:

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

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

The "not" of Prolog's "negation as failure" already means not(true(LP))
when we assume that true(LP) means provable(LP).

>>>> Maybe if you will think
>>>> hard enough you can make it detect such conditions, probably by writing
>>>> meta-interpreter of some sort, and terminate. Personally, I don't think
>>>> that using Prolog can be accepted as a "rigorous proof" of anything.
>>>
>>> That's just nonsense: Prolog is a formal language no less than any other.
>>> Plus you too must think you have a solution to the halting problem...
>>
>> No, I don't have a solution for a halting problem, I'm not a freak, but
>> also solving termination for _some_ specially designed simple programs
>> doesn't require halting problem. It's some first grader stuff, c'mon.
>
> You bring it up: and it is in fact irrelevant here, as long as the
> original question is the question you noticed it is.
>
> Anyway, discussing with Olcott's interlocutors is always even
> worse than discussing with Olcott himself...
>
> (EOD.)
>
> Julio

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 12:38 PM, Aleksy Grabowski wrote:
> On 5/2/22 18:51, Julio Di Egidio wrote:
>> On Monday, 2 May 2022 at 18:38:10 UTC+2, Aleksy Grabowski wrote:
>>> On 5/2/22 18:04, olcott wrote:
>>>
>>>> Is there any Prolog that can detect that the above will not terminate
>>>> prior to executing it?
>>>
>>> As I have said previously, my example is naïve.
>>
>> And as I have pointed out to you, your "solution" solves nothing at all.
>
> The request from topic poster was — how would I represent sentence "This
> sentence is not provable". I came up with some small example of "not
> provable sentence"

I would say that you did an excellent job of that.
What do you think of this version:

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

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

The "not" of Prolog's "negation as failure" already means not(true(LP))
when we assume that true(LP) means provable(LP).

> which happens to be a simple infinite loop. I did
> *not* claim that it captures anything deep and solves halting problem,
> that would've been absurd. If you have any better idea please write it.
>
>>> Maybe if you will think
>>> hard enough you can make it detect such conditions, probably by writing
>>> meta-interpreter of some sort, and terminate. Personally, I don't think
>>> that using Prolog can be accepted as a "rigorous proof" of anything.
>>
>> That's just nonsense: Prolog is a formal language no less than any other.
>> Plus you too must think you have a solution to the halting problem...
>
> No, I don't have a solution for a halting problem, I'm not a freak, but
> also solving termination for _some_ specially designed simple programs
> doesn't require halting problem. It's some first grader stuff, c'mon.
>
> Like this random example from my head (in C++):
>
>     int sum = 0;
>     for (int i = 5; i > 0; i--)
>         sum += i;
>
> Can be proved to always terminate, because loop's variant `i` has lower
> bound, has total ordering and it's value decreases on each iteration. In
> some cases you can automatically detect such loop variants, and
> automatically prove termination of _some_ loops.
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 1:41 PM, Mr Flibble wrote:
> On Mon, 2 May 2022 11:28:23 -0600
> Jeff Barnett <jbb@notatt.com> wrote:
>
>> On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE
>>
>>
>> I will attempt to summarize the level of the idiot's understanding of
>> Prolog: The level is the same as of his understanding of math, logic,
>> C, C++, software engineering, programming, programming methodology,
>> Turing Machines, and other specific topics in these general
>> categories. He is capable of moving his eyes through a few paragraphs
>> but not reading anything. This is a common learning disability. He
>> can cut and paste from what little is eyes scan but, in general, he
>> can neither comprehend the little he's seen nor can he amalgamate
>> concepts from the bits and pieces he has visited.
>>
>> His approach to gaining and demonstrating understanding is best
>> represented by a comic's view of monkeys exploring objects new to
>> them: biting things, hitting other objects with the new one, stirring
>> feces and seeing if it will stick and can be thrown etc. The problem
>> with this metaphor is that monkeys are intelligent and our idiot is
>> not. When the monkey is done with initial exploration, it has an idea
>> whether the new object can serve some useful purpose; in any event,
>> the monkey had fun. The idiot, on the other hand, never discoveries
>> the usefulness of the potential new knowledge because he doesn't have
>> the attention span or curiosity to do so. That's why he is an idiot
>> and not as smart or as wise as the monkey though he too has fun.
>
> The ad hominem attack is a logical fallacy: so it is in fact YOU who is
> throwing excrement at the walls, not Olcott. Attack the argument not the
> person, dear.
>
> https://en.wikipedia.org/wiki/Ad_hominem
>
> /Flibble
>

Yes Jeff is mostly a Jackass. Once in a very great while he says
something interesting. This is very rare yet thankfully more often than
never.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 12:28 PM, Jeff Barnett wrote:
> On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE
>
>
> I will attempt to summarize the level of the idiot's understanding of
> Prolog: The level is the same as of his understanding of math, logic, C,
> C++, software engineering, programming, programming methodology, Turing
> Machines, and other specific topics in these general categories. He is
> capable of moving his eyes through a few paragraphs but not reading
> anything. This is a common learning disability. He can cut and paste
> from what little is eyes scan but, in general, he can neither comprehend
> the little he's seen nor can he amalgamate concepts from the bits and
> pieces he has visited.
>
> His approach to gaining and demonstrating understanding is best
> represented by a comic's view of monkeys exploring objects new to them:
> biting things, hitting other objects with the new one, stirring feces
> and seeing if it will stick and can be thrown etc. The problem with this
> metaphor is that monkeys are intelligent and our idiot is not. When the
> monkey is done with initial exploration, it has an idea whether the new
> object can serve some useful purpose; in any event, the monkey had fun.
> The idiot, on the other hand, never discoveries the usefulness of the
> potential new knowledge because he doesn't have the attention span or
> curiosity to do so. That's why he is an idiot and not as smart or as
> wise as the monkey though he too has fun.

My key more important understanding of the fundamental architecture of
Prolog is that it is anchored in sound deductive inference thus
correctly all of the errors that have crept into logic since Aristotle's
syllogism.

Start with known truths (Prolog facts) and only apply truth preserving
operations (Prolog rules) to derive conclusions that can be relied on as
true.

Also helpful is Prolog's negation as failure that does not make the huge
mistake of assuming that every expression that is not true must be 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

On 5/2/22 21:24, olcott wrote:
> What do you think of this version:
>
> ?- LP = not(LP).
> LP = not(LP).

In this expression, `not` is treated as a term — a symbol without any
meaning, just text "not", and not the _negation_.

If you want to check if a variable can be different from itself you can
try this:

?- dif(X, X).

But, remember that dif/2 isn't available in all Prolog implementations.

--
Alex Grabowski

On 5/2/2022 2:43 PM, Aleksy Grabowski wrote:
> On 5/2/22 21:24, olcott wrote:
>> What do you think of this version:
>>
>> ?- LP = not(LP).
>> LP = not(LP).
>
> In this expression, `not` is treated as a term — a symbol without any
> meaning, just text "not", and not the _negation_.
>

(SWI-Prolog (threaded, 64 bits, version 7.6.4)
Predicate not/1

not(:Goal)
True if Goal cannot be proven. Retained for compatibility only. New code
should use \+/1.

https://www.swi-prolog.org/pldoc/man?predicate=not/1

SWI Prolog does not accept this, did I say it incorrectly?
?- g :- \+ g.
?- g.

> If you want to check if a variable can be different from itself you can
> try this:
>
>     ?- dif(X, X).
>
> But, remember that dif/2 isn't available in all Prolog implementations.
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/22 22:10, olcott wrote:
> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
> Predicate not/1
>
> not(:Goal)
> True if Goal cannot be proven. Retained for compatibility only. New code
> should use \+/1.
>
> https://www.swi-prolog.org/pldoc/man?predicate=not/1
>
> SWI Prolog does not accept this, did I say it incorrectly?
> ?- g :- \+ g.
> ?- g.

You have said it incorrectly. Prolog program has two different parts:
knowledge base and a query.

Knowledge base is usually loaded from the text file before starting
Prolog runtime.

Query can be asked using interactive prompt.

The general distinction is that knowledge base should contain everything
that is known, and query is used to ask questions to that database.

> ?- g :- \+ g.

This expression asks a question (note question mark), which isn't
correct, it should be stated as a fact.

Quick and dirty way to add facts dynamically is to use very special
`assertz/1` predicate. Like this:

?- assertz( (g :- \+ g) ).
true.

Then you can normally ask a question:

?- g.

This question causes infinite loop, so you will never see an answer,
which is correct.

There are couple of strategies to detect infinite recursion in some very
limited number of predicates, but they are quite advanced and probably
we don't want to go there.

--
Alex Grabowski

On 5/2/2022 3:37 PM, Aleksy Grabowski wrote:
> On 5/2/22 22:10, olcott wrote:
>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>> Predicate not/1
>>
>> not(:Goal)
>> True if Goal cannot be proven. Retained for compatibility only. New
>> code should use \+/1.
>>
>> https://www.swi-prolog.org/pldoc/man?predicate=not/1
>>
>> SWI Prolog does not accept this, did I say it incorrectly?
>> ?- g :- \+ g.
>> ?- g.
>
> You have said it incorrectly. Prolog program has two different parts:
> knowledge base and a query.
>
> Knowledge base is usually loaded from the text file before starting
> Prolog runtime.
>
> Query can be asked using interactive prompt.
>
> The general distinction is that knowledge base should contain everything
> that is known, and query is used to ask questions to that database.
>
>> ?- g :- \+ g.
>
> This expression asks a question (note question mark), which isn't
> correct, it should be stated as a fact.
>
> Quick and dirty way to add facts dynamically is to use very special
> `assertz/1` predicate. Like this:
>
>     ?- assertz( (g :- \+ g) ).
>     true.
>
> Then you can normally ask a question:
>
>     ?- g.
>
> This question causes infinite loop, so you will never see an answer,
> which is correct.
>

I do see that it is rejected by SWI Prolog:

?- assertz( (g :- \+ g) ).
true.

?- g.
ERROR: Out of local stack
?-

> There are couple of strategies to detect infinite recursion in some very
> limited number of predicates, but they are quite advanced and probably
> we don't want to go there.
>

This one seems to work:

?- LP = \+(true(LP)).
LP = (\+true(LP)).

?- unify_with_occurs_check(LP, \+(true(LP))).
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

On 5/2/2022 3:58 PM, olcott wrote:
> On 5/2/2022 3:37 PM, Aleksy Grabowski wrote:
>> On 5/2/22 22:10, olcott wrote:
>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>> Predicate not/1
>>>
>>> not(:Goal)
>>> True if Goal cannot be proven. Retained for compatibility only. New
>>> code should use \+/1.
>>>
>>> https://www.swi-prolog.org/pldoc/man?predicate=not/1
>>>
>>> SWI Prolog does not accept this, did I say it incorrectly?
>>> ?- g :- \+ g.
>>> ?- g.
>>
>> You have said it incorrectly. Prolog program has two different parts:
>> knowledge base and a query.
>>
>> Knowledge base is usually loaded from the text file before starting
>> Prolog runtime.
>>
>> Query can be asked using interactive prompt.
>>
>> The general distinction is that knowledge base should contain
>> everything that is known, and query is used to ask questions to that
>> database.
>>
>>> ?- g :- \+ g.
>>
>> This expression asks a question (note question mark), which isn't
>> correct, it should be stated as a fact.
>>
>> Quick and dirty way to add facts dynamically is to use very special
>> `assertz/1` predicate. Like this:
>>
>>      ?- assertz( (g :- \+ g) ).
>>      true.
>>
>> Then you can normally ask a question:
>>
>>      ?- g.
>>
>> This question causes infinite loop, so you will never see an answer,
>> which is correct.
>>
>
> I do see that it is rejected by SWI Prolog:
>
> ?- assertz( (g :- \+ g) ).
> true.
>
> ?- g.
> ERROR: Out of local stack
> ?-
>
>> There are couple of strategies to detect infinite recursion in some
>> very limited number of predicates, but they are quite advanced and
>> probably we don't want to go there.
>>
>

Here it is even simpler:

?- LP = \+(LP).
LP = (\+LP).

?- unify_with_occurs_check(LP, \+(LP)).
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

On 5/2/22 22:58, olcott wrote:
> This one seems to work:
>
> ?- LP = \+(true(LP)).
> LP =  (\+true(LP)).
>
> ?- unify_with_occurs_check(LP, \+(true(LP))).
> false.

Sadly you aren't using Prolog correctly. You still have to *execute*
predicates, because right now they don't mean anything. You can try to
enable predicate tracer and see for yourself that neither \+ nor `true`
is ever executed.

To enable tracer issue following command in the prompt:

?- trace.
true.

Then you can run your queries again. Then don't forget to disable
tracer, by issuing command:

?- notrace.
true.

Also, Prolog doesn't define true/1 predicate it defines only true/0
without any arguments. First of all you need to define it:

?- assertz( (true(X) :- call(X)) ).

Then still you need to execute your goals by using special call/1 predicate.

?- LP = \+(true(LP)), call(LP).

With occurs check you will see that it will fail even sooner, and it
wont be even executed.

--
Alex Grabowski

On 5/2/2022 4:33 PM, Aleksy Grabowski wrote:
> On 5/2/22 22:58, olcott wrote:
>> This one seems to work:
>>
>> ?- LP = \+(true(LP)).
>> LP =  (\+true(LP)).
>>
>> ?- unify_with_occurs_check(LP, \+(true(LP))).
>> false.
>
> Sadly you aren't using Prolog correctly. You still have to *execute*
> predicates, because right now they don't mean anything. You can try to
> enable predicate tracer and see for yourself that neither \+ nor `true`
> is ever executed.
>
> To enable tracer issue following command in the prompt:
>
>     ?- trace.
>     true.
>
> Then you can run your queries again. Then don't forget to disable
> tracer, by issuing command:
>
>     ?- notrace.
>     true.
>
> Also, Prolog doesn't define true/1 predicate it defines only true/0
> without any arguments. First of all you need to define it:
>
>    ?- assertz( (true(X) :- call(X)) ).
>
> Then still you need to execute your goals by using special call/1
> predicate.
>
>    ?- LP = \+(true(LP)), call(LP).
>
> With occurs check you will see that it will fail even sooner, and it
> wont be even executed.
>

That is why I updated it to this:

?- LP = \+(LP).
LP = (\+LP).

?- unify_with_occurs_check(LP, \+(LP)).
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

On 5/2/22 23:42, olcott wrote:
> That is why I updated it to this:
>
> ?- LP = \+(LP).
> LP =  (\+LP).
>
> ?- unify_with_occurs_check(LP, \+(LP)).
> false.
>

This still is incorrect.

First of all, enable tracing:

?- trace.
true.

Then *execute* the predicates that you are trying to use:

[trace] ?- LP = \+(LP), call(LP).
Call: (11) _6566=(\+_6566) ? creep
Exit: (11) (\+ \+ \+ \+ \+ \+ \+ \+ \+ ...)=(\+ \+ \+ \+ \+ \+
\+ \+ \+ ...) ? creep
ERROR: Cannot represent due to `cyclic_term'
ERROR: In:
ERROR: [10] '<meta-call>'(user:user: ...)
ERROR: [9] toplevel_call(user:user: ...)

Which will throw an exception, because Prolog can't deal with it.

If you will try to unify without occurs check:

[trace] ?- unify_with_occurs_check(LP, \+(LP)), call(LP).
Call: (11) unify_with_occurs_check(_1010, \+_1010) ? creep
Fail: (11) unify_with_occurs_check(_1010, \+_1010) ? creep
false.

Then you will see, that your operator \+ isn't even mentioned, as it
wasn't executed by the Prolog system, because unification with occurs
check doesn't work for self referential terms. The whole reason of
occurs check is to reject such terms, this is why this check was added
in the first place.

--
Alex Grabowski

On 5/2/22 3:32 PM, olcott wrote:
> On 5/2/2022 12:28 PM, Jeff Barnett wrote:
>> On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE
>>
>>
>> I will attempt to summarize the level of the idiot's understanding of
>> Prolog: The level is the same as of his understanding of math, logic,
>> C, C++, software engineering, programming, programming methodology,
>> Turing Machines, and other specific topics in these general
>> categories. He is capable of moving his eyes through a few paragraphs
>> but not reading anything. This is a common learning disability. He can
>> cut and paste from what little is eyes scan but, in general, he can
>> neither comprehend the little he's seen nor can he amalgamate concepts
>> from the bits and pieces he has visited.
>>
>> His approach to gaining and demonstrating understanding is best
>> represented by a comic's view of monkeys exploring objects new to
>> them: biting things, hitting other objects with the new one, stirring
>> feces and seeing if it will stick and can be thrown etc. The problem
>> with this metaphor is that monkeys are intelligent and our idiot is
>> not. When the monkey is done with initial exploration, it has an idea
>> whether the new object can serve some useful purpose; in any event,
>> the monkey had fun. The idiot, on the other hand, never discoveries
>> the usefulness of the potential new knowledge because he doesn't have
>> the attention span or curiosity to do so. That's why he is an idiot
>> and not as smart or as wise as the monkey though he too has fun.
>
> My key more important understanding of the fundamental architecture of
> Prolog is that it is anchored in sound deductive inference thus
> correctly all of the errors that have crept into logic since Aristotle's
> syllogism.
>
> Start with known truths (Prolog facts) and only apply truth preserving
> operations (Prolog rules) to derive conclusions that can be relied on as
> true.
>
> Also helpful is Prolog's negation as failure that does not make the huge
> mistake of assuming that every expression that is not true must be false.
>

IF you are defining that your logic system is limited to what Prolog can
"Prove", that is fine. Just realize that you have just defined that your
logic system can't handle a lot of the real problems in the world, and
in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to
handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in
expressibility.

On 5/2/22 9:19 AM, olcott wrote:
> On 5/2/2022 6:10 AM, Richard Damon wrote:
>> On 5/1/22 11:04 PM, olcott wrote:
>>> On 5/1/2022 9:47 PM, Richard Damon wrote:
>>>> On 5/1/22 10:18 PM, olcott wrote:
>>>>> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>>>>>
>>>>>> On 5/1/22 9:53 PM, olcott wrote:
>>>>>>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>>>>>>> On 5/1/22 8:58 PM, olcott wrote:
>>>>>>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>>>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> So which categories are you claiming are
>>>>>>>>>>>>>>>>>>>>>>>> involved? Claiming something is a 'category
>>>>>>>>>>>>>>>>>>>>>>>> error' means nothing if you don't specify the
>>>>>>>>>>>>>>>>>>>>>>>> actual categories involved.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the
>>>>>>>>>>>>>>>>>>>>>>> Liar Paradox all demonstrate the exact same
>>>>>>>>>>>>>>>>>>>>>>> error. I only have considered (3) in recent
>>>>>>>>>>>>>>>>>>>>>>> years, prior to that I never heard of (3).
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> The category error would be that none of them is
>>>>>>>>>>>>>>>>>>>>>>> in the category of truth bearers. For Gödel's G
>>>>>>>>>>>>>>>>>>>>>>> and Tarski's p it would mean that the category
>>>>>>>>>>>>>>>>>>>>>>> error is that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before
>>>>>>>>>>>>>>>>>>>>> you bother to notice that I said it once?
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be
>>>>>>>>>>>>>>>>>>>>> used for a similar undecidability proof
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> And what does any of the above have to do with what
>>>>>>>>>>>>>>>>>>>> I state below? That's your faulty attempt at
>>>>>>>>>>>>>>>>>>>> expressing The Liar in Prolog, which has nothing to
>>>>>>>>>>>>>>>>>>>> do with Gödel's G. G has *a relationship* to The
>>>>>>>>>>>>>>>>>>>> Liar, but G is *very* different from The Liar in
>>>>>>>>>>>>>>>>>>>> crucial ways.
>>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be
>>>>>>>>>>>>>>>>>>> used for a similar
>>>>>>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a
>>>>>>>>>>>>>>>>>>> similar
>>>>>>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge
>>>>>>>>>>>>>>>>> of the strawman error.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Do you understand the difference between 'close
>>>>>>>>>>>>>>>> relationship' and 'the same'?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> The only one being dishonest here is you as you keep
>>>>>>>>>>>>>> snipping the substance of my post.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Gödel claims there is a *close relationship* between The
>>>>>>>>>>>>>> Liar and G. He most certainly does *not* claim that they
>>>>>>>>>>>>>> are the same. (That one can construct similar proofs which
>>>>>>>>>>>>>> bear a similar close relationship to other antinomies is
>>>>>>>>>>>>>> hardly relevant since it is The Liar which is under
>>>>>>>>>>>>>> discussion).
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> (a) G does *not* assert its own unprovability whereas The
>>>>>>>>>>>>>> Liar *does* assert its own falsity.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar
>>>>>>>>>>>>>> is not.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm
>>>>>>>>>>>>>> not going to retype my explanation for this as I have
>>>>>>>>>>>>>> already given it in a previous post. You're more than
>>>>>>>>>>>>>> welcome to go back and read that post. Unless you actually
>>>>>>>>>>>>>> have some comment on that explanation, there's no point
>>>>>>>>>>>>>> repeating yourself.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>> a similar undecidability proof
>>>>>>>>>>>>>
>>>>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy
>>>>>>>>>>>>> you lying bastard.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> So, there is a difference between being used for and being
>>>>>>>>>>>> just like.
>>>>>>>>>>>
>>>>>>>>>>> sufficiently equivalent
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> You can PROVE it?
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> I backed André into a corner and forced him to quit lying
>>>>>>>>>
>>>>>>>>
>>>>>>>> So, No. Note a trimming to change meaning, the original was:
>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>>
>>>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy
>>>>>>>>>>>> you lying bastard.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> So, there is a difference between being used for and being
>>>>>>>>>>> just like.
>>>>>>>>>>
>>>>>>>>>> sufficiently equivalent
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> You can PROVE it?
>>>>>>>>
>>>>>>>> So, clearly the requested proof was that about USING the
>>>>>>>> epistemolgocal antinomy and it being just like one so not a
>>>>>>>> Truth Bearer. Note, the comment that you claimed you backed him
>>>>>>>> into isn't about that, so you are just proving yourself to be a
>>>>>>>> deciver.
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>>>>>>  > Yes. The Liar and the Liar can be used for similar
>>>>>>>>> undecidability
>>>>>>>>>  > proofs. I have no idea what it is you hope to achieve by
>>>>>>>>> arguing for a
>>>>>>>>>  > truism.
>>>>>>>>>
>>>>>>>>
>>>>>>>> Nice out of context quoting, showing again you are the deciver.
>>>>>>>
>>>>>>> If you look at the full context of many messages you will see
>>>>>>> that he kept continuing to deny that the Liar Paradox can be used
>>>>>>> for similar undecidability proofs at least a half dozen times.
>>>>>>> Only when I made denying this look utterly ridiculously foolish
>>>>>>> did he finally quit lying about it.
>>>>>>>
>>>>>>
>>>>>> No, he says that the use of the Liar Paradox in the form that
>>>>>> Godel does doesn't make the Godel Sentence a non-truth holder.
>>>>>>
>>>>>
>>>>> If you look at the actual facts you will see that he continued to
>>>>> deny that kept continuing to deny that the Liar Paradox can be used
>>>>> for similar undecidability proofs at least a half dozen times.
>>>>>
>>>>> If you make sure to knowingly contradict the verified facts then
>>>>> Revelations 21:8 may eventually apply to you.
>>>>>
>>>>
>>>> You mean like when he said (and you snipped):
>>>>
>>>>>
>>>>> The only one being dishonest here is you as you keep snipping the
>>>>> substance of my post.
>>>>>
>>>>> Gödel claims there is a *close relationship* between The Liar and
>>>>> G. He most certainly does *not* claim that they are the same. (That
>>>>> one can construct similar proofs which bear a similar close
>>>>> relationship to other antinomies is hardly relevant since it is The
>>>>> Liar which is under discussion).
>>>>>
>>>>> There are two crucial differences between G and The Liar:
>>>>>
>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>> *does* assert its own falsity.
>>>>>
>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>
>>>>> Your claim the Gödel's theorem is a 'category error' is predicated
>>>>> on the fact that you don't grasp (b) above. I'm not going to retype
>>>>> my explanation for this as I have already given it in a previous
>>>>> post. You're more than welcome to go back and read that post.
>>>>> Unless you actually have some comment on that explanation, there's
>>>>> no point repeating yourself.
>>>>>
>>>>
>>>> Maybe you should check your OWN facts.
>>>>
>>>
>>> He is focusing on the dishonest dodge of the strawman error by making
>>> sure to ignore that in another quote Gödel said that Gödel's G is
>>> sufficiently equivalent to the Liar Paradox on the basis that the
>>> Liar Paradox is an epistemological antinomy, whereas the quote he
>>> keeps switching back to is less clear on this point.
>>>
>>> Since I focused on correcting his mistake several times it finally
>>> got down to the point where it was clear that he was a lying bastard.
>>>
>>> I am utterly immune to gas lighting.
>>>
>>>> He is CLEARLY not saying that the Liar Paradox can't be used for
>>>> this sort of proof, because he talks about its form being used.
>>>>
>>>
>>> He continued to refer to the other quote of Gödel that is much more
>>> vague on the equivalence between Gödel's G as his basis that
>>> equivalence cannot be be determined even when I kept focusing him
>>> back on the quote that does assert sufficient equivalence exists. I
>>> did this six times.
>>>
>>> At this point my assessment that he was a lying bastard was
>>> sufficiently validated.
>>>
>>> Are you a lying bastard too, or will you acknowledge that my
>>> assessment is correct?
>>>
>>
>> I will acknowledge that you have proven yourself to be the lying bastard.
>>
>> YOU have REPEADTEDLY trimmed out important parts of the conversation
>> either to INTENTIONALLY be deceptive, or because you are so
>> incompetent at this material that you don't know what is important.
>>
>
> I trim so that we can stay focused on the point at hand and not diverge
> into many unrelated points. The main way that all of the rebuttals of my
> work are formed is changing the subject to another different subject and
> the rebutting this different subject. I cut all that bullshit out.

> IF you are defining that your logic system is limited to what Prolog can
> "Prove", that is fine. Just realize that you have just defined that your
> logic system can't handle a lot of the real problems in the world, and
> in particular, it is very limited in the mathematics it can handle.
>
> I am pretty sure that Prolog is NOT up to handling the logic needed to
> handle the mathematics needed to express Godel's G, or the Halting Problem.
>
> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
> have only proven that your limited logic system can't reach them in
> expressibility.
>

Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form is
a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.

--
Alex Grabowski

On Tuesday, 3 May 2022 at 00:41:18 UTC+2, Aleksy Grabowski wrote:
> On Tuesday, 3 May 2022 at 00:38:57 UTC+2, Richard Damon wrote:
> > IF you are defining that your logic system is limited to what Prolog can
> > "Prove", that is fine. Just realize that you have just defined that your
> > logic system can't handle a lot of the real problems in the world, and
> > in particular, it is very limited in the mathematics it can handle.
> >
> > I am pretty sure that Prolog is NOT up to handling the logic needed to
> > handle the mathematics needed to express Godel's G, or the Halting Problem.
> >
> > Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
> > have only proven that your limited logic system can't reach them in
> > expressibility.
> >
> Thanks for confirmation, that's what exactly what I was trying to tell
> to topic poster in one of my previous posts. Prolog in it's bare form is
> a bad theorem solver. It wasn't designed a such.
>
> If you want to deal with such problems maybe it is better to use Coq
> theorem prover, I've never used it by myself, but it looks like one of
> the best proving assistants out there.

Prolog is a Turing-complete language, duh.
When Dunning-Kruger is a compliment...

Get the fuck out of comp.lang.prolog.

*Plonk*

Julio

On 5/3/22 01:00, Julio Di Egidio wrote:
> Prolog is a Turing-complete language, duh.
> When Dunning-Kruger is a compliment...
>
> Get the fuck out of comp.lang.prolog.
>
> *Plonk*
>
> Julio

I've already wrote it in one of my previous posts, I just didn't want to
repeat myself:

> Prolog *by itself* is a very bad theorem prover and it is very limited
> framework for formal logic, because it implements only Horn clauses.
> However it is a very good programming language and you can implement
> any theorem prover in it, like you can implement any theorem prover
> in C++ or Java.

I probably have found your profile on the internet and I conclude that
your arrogance directly stems from your lack of any formal education.
You didn't graduate from any high school and that's why you want to show
everybody your perceived superiority.

I'll just ignore you for the time being.

--
Alex Grabowski

Aleksy Grabowski <hurufu@gmail.com> writes:

>> IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your
>> logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>> handle the mathematics needed to express Godel's G, or the Halting Problem.
>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>> have only proven that your limited logic system can't reach them in expressibility.
>
> Thanks for confirmation, that's what exactly what I was trying to tell
> to topic poster in one of my previous posts. Prolog in it's bare form
> is a bad theorem solver. It wasn't designed a such.
>
> If you want to deal with such problems maybe it is better to use Coq
> theorem prover, I've never used it by myself, but it looks like one of
> the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).

--
Ben.

On 5/2/2022 5:41 PM, Aleksy Grabowski wrote:
>> IF you are defining that your logic system is limited to what Prolog
>> can "Prove", that is fine. Just realize that you have just defined
>> that your logic system can't handle a lot of the real problems in the
>> world, and in particular, it is very limited in the mathematics it can
>> handle.
>>
>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>> handle the mathematics needed to express Godel's G, or the Halting
>> Problem.
>>
>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>> have only proven that your limited logic system can't reach them in
>> expressibility.
>>
>
> Thanks for confirmation, that's what exactly what I was trying to tell
> to topic poster in one of my previous posts. Prolog in it's bare form is
> a bad theorem solver. It wasn't designed a such.
>
> If you want to deal with such problems maybe it is better to use Coq
> theorem prover, I've never used it by myself, but it looks like one of
> the best proving assistants out there.
>

I might take a look at it. The key advantage of Prolog that that by
basing its analysis on facts and rules and having negation as failure it
corrects all of the errors of formal logic systems.

Prolog does not make the mistake of assuming that when an expression is
not true that it must be false. Because of this Prolog can detect
semantically ill-formed expressions that formal logic simply assumes are
correct.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer