Liste des Groupes | Revenir à theory |
On 5/29/2024 2:01 AM, Python wrote:Which has NOTHING to do with the statement you are replying to, showing your utter stupidity.Le 29/05/2024 à 04:39, olcott a écrit :?- LP = not(true(L, LP)).
...>>That Prolog construes any expression having the same structure as the>
Liar Paradox as having a cycle in the directed graph of its evaluation
sequence already completely proves my point. In other words Prolog
is saying that there is something wrong with the expression and it must
be rejected.
But Prolog doesn't support powerful enough logic to handle the system like Tarski and Godel are talking about.
>
The fact that Prolog just rejects it shows that.
>
Your ignorance is no excuse.
You, Peter Olcott, are actually the one showing one's ignorance here.
>
Gödel theorems can be handled by more powerful proving systems such
as COQ : http://r6.ca/Goedel/goedel1.html
LP = not(true(L, LP)).
?- unify_with_occurs_check(LP, not(true(L, LP))).
false.
Richard explained this incorrectly.
let's see if you can do better.
I created Minimal Type Theory that does the same thing as
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Minimal Type Theory (YACC BNF)
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
LP := ~True(L, LP)
definition_2 token="ASSIGN_ALIAS"
| definition_2 token="IDENTIFIER" value="LP"
| sentence_2 token="NOT"
| | atomic_sentence_1 token="IDENTIFIER" value="True"
| | | term_list_1
| | | | term_2 token="IDENTIFIER" value="L"
| | | | term_2 token="IDENTIFIER" value="LP"
<definition_2 token="ASSIGN_ALIAS">
<definition_2 token="IDENTIFIER" value="LP"/>
<sentence_2 token="NOT">
<atomic_sentence_1 token="IDENTIFIER" value="True">
<term_list_1>
<term_2 token="IDENTIFIER" value="L"/>
<term_2 token="IDENTIFIER" value="LP"/>
</term_list_1>
</atomic_sentence_1>
</sentence_2>
</definition_2>
Directed graph of evaluation sequence of LP
Nodes on the left edges on the right
00 NOT 01
01 True 02, 00 // cycle
02 L
Les messages affichés proviennent d'usenet.