I guess there is a bug in preparing flat terms vector
I give you a gold medal 🥇, if you can prove a
compare_index/3 correct that uses this rule. It
was already shown impossible by Matt Carlson.
There are alternative approaches that can reach
transitivity, but do not use the below step
inside some compare_index/3.
compare_term_args(I, C, X, Y, A, H):-
arg(I, X, K),
arg(I, Y, L),
!,
compare_index(D, K, L, A, H),
( D = (=) ->
I0 is I + 1,
compare_term_args(I0, C, X, Y, A, H)
; C = D
).
compare_term_args(_ ,= , _, _, _, _).
Maybe there is a grain of salt of invoking the
Axiom of Choice (AC) in some previous posts.
Although the Axiom of Choice is not needed for
finite sets, they have anyway some choice.
BTW: When Peter Aczel writes ZFC-, he then
means ZFC without AC, right? But he doesn’t
show some compare/3 .
Mild Shock schrieb:
Hi,
Take this exercise. Exercise 4.1 Draw the tree
represented by the term n1(n2(n4),n3(n5,n6)). https://book.simply-logical.space/src/text/2_part_ii/4.1.html
Maybe there was a plan that SWISH can draw trees,
and it could be that something was implemented as well.
But I don't see anything dynamic working on the
above web site link. Next challenge for Simply Logical,
in another life. Draw a rational tree.
The Prolog system has them:
/* SWI-Prolog 9.3.26 */
?- X = a(Y,_), Y = b(X,_).
X = a(b(X, _A), _),
Y = b(X, _A).
Bye
Mild Shock schrieb:
Hi,
My beloved Logic professor introduced Non-Wellfounded
in the form of library cards, sorry only German:
Wir denken uns dazu eine Kartothek, auf deren
Karten wieder Karten derselben Kartothek
aufgeführt sind. Ein Beispiel einer solchen
Kartothek wäre etwa das folgende : wir haben
drei Karten a, b, c; a führt a und b auf, b
die Karten a und c, c die Karte b a = (a, b),
b = (a, c), c = (b). Entsprechend den sich
nicht selbst als Element enthaltenden Mengen
fragen wir nach den Karten, die sich nicht
selbst aufführen. Die Karte a ist die einzige,
die sich selbst aufführt ; b und c sind somit
die sich nicht selbst aufführenden Karten.
He then concludes that Non-Wellfounded has still the
Russell Paradox, and hence also the productive form of it:
Es gibt somit in jeder Kartothek eine
Gesamtheit G von Karten, zu der es keine Karte
gibt, die genau jene aus G aufführt. (Für endliche
Kartotheken ist dies ziemlich selbstverständlich,
doch wollen wir auch unendliche Kartotheken in
Betracht ziehen.) Dieser Satz schliesst aber
natürlich nicht aus, dass es stets möglich ist,
eine genau die Karten aus G aufführende Karte
herzustellen und diese in die Kartothek zu legen.
Nur müssen wir mit der Möglich-
What is your opinion? Excerpt from:
**DIE ANTINOMIEN DER MENGENLEHRE**
E. Specker, Dialectica, Vol. 8, No. 3 (15. 9. 1954)
https://www.jstor.org/stable/42964119?seq=7
Bye
Mild Shock schrieb:
Hi,
That is extremly embarassing. I don’t know
what you are bragging about, when you wrote
the below. You are wrestling with a ghost!
Maybe you didn’t follow my superbe link:
seemingly interesting paper. In stead
particular, his final coa[l]gebra theorem
The link behind Hopcroft and Karp (1971) I
gave, which is a Bisimulation and Equirecursive
Equality hand-out, has a coalgebra example,
I used to derive pairs.pl from:
https://www.cs.cornell.edu/courses/cs6110/2014sp/Lectures/lec35a.pdf
Bye
Mild Shock schrieb:
Inductive logic programming at 30
https://arxiv.org/abs/2102.10556
The paper contains not a single reference to autoencoders!
Still they show this example:
Fig. 1 ILP systems struggle with structured examples that
exhibit observational noise. All three examples clearly
spell the word "ILP", with some alterations: 3 noisy pixels,
shifted and elongated letters. If we would be to learn a
program that simply draws "ILP" in the middle of the picture,
without noisy pixels and elongated letters, that would
be a correct program.
I guess ILP is 30 years behind the AI boom. An early autoencoder
turned into transformer was already reported here (*):
SERIAL ORDER, Michael I. Jordan - May 1986
https://cseweb.ucsd.edu/~gary/PAPER-SUGGESTIONS/Jordan-TR-8604-OCRed.pdf >>>>
Well ILP might have its merits, maybe we should not ask
for a marriage of LLM and Prolog, but Autoencoders and ILP.
But its tricky, I am still trying to decode the da Vinci code of
things like stacked tensors, are they related to k-literal clauses?
The paper I referenced is found in this excellent video:
The Making of ChatGPT (35 Year History)
https://www.youtube.com/watch?v=OFS90-FX6pg
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)