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

Groups > sci.physics > #895954

Buddos Waterloo: Checkpoint McCune (Re: Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS)

Cross-posted to 2 groups.

Show all headers | View raw

Hi,

Now toying around with a model finder,
for some rewritng problems. Not bad, I
didn't see that before on my computer:

?- time(mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, _)).
% Zeit 166.140 ms, GC 0.000 ms, Lips 18616 k
true

?- mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, R).
R = [d-2, c-1, 5*2-3, 5*5-4, 4*3-2, 3*5-2, 3*2-5, 4*4-5, 2*4-3,
2*3-4, 3*4-1, 3*1-4, 5*3-1, 4*1-3, 1*5-3, 1*3-5, 2*1-5, 2*5-1,
5*1-2, 4*2-1, 1*4-2, 1*2-4, 5*0-5, 4*0-4, 4*5-0, 5^ -1-4, 5*4-0,
4^ -1-5, 3*0-3, 3*3-0, 3^ -1-3, 2*0-2, 2*2-0, 2^ -1-2, 1*0-1,
1*1-0, 1^ -1-1, 0^ -1-0, 0*5-5, 0*4-4, 0*3-3, 0*2-2,
0*1-1, 0*0-0, e-0]

But still not as good as Mc Cune, wo reported
0.010 seconds , so 10 ms (*). I guess I need to
explore more heuristics. But will it include

union find? The payback of union find in such
search examples is so low. If |D| = n is the
domain size, then although |D x D| has size n^2,

the diagonal E_D, namely E_D = { (x,y) | x e D,
y e D, x = y } has only size n. So the probability
of a pair in certain problem domains, is around 1/n,

getting smaller and smaller with larger and larger n.

Bye

(*)
https://www.mcs.anl.gov/research/projects/AR/mace4/July-2005/doc/mace4.pdf

Mild Shock schrieb:
> Hi,
> 
> This is a nice example how the young generation
> doesn't understand systems that were developed
> 30 years ago:
> 
> Example 1:
> No clue that SWI-Prolog does have JIT indexes,
> which explain mysterious differene between
> cold and warm run.
> https://arxiv.org/pdf/2511.13600
> 
> Example 2:
> No clue that subsumption could make a difference,
> claims left recursion is fastest, with referene
> to [TL10] and a bogus node argument.
> https://arxiv.org/abs/2504.21291
> 
> Maybe the Prolog eduction group should organize
> a summer school about tabling?
> 
> Sad news: It will not help to keep up with
> the AI boom. Whats behind the AI boom and
> computing transitive closures?
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Ok, thats noice:
>>
>> "On a GPU cluster, the ratio of high computing
>> power to communication bandwidth makes scaling
>> breadth-first search (BFS) on a scale-free
>> graph extremely challenging."
>>
>> Scalable Breadth-First Search on a GPU Cluster
>> Yuechao Pan, Roger Pearce, John D. Owens
>> 2018 - Lawrence Livermore National Laboratory
>> https://arxiv.org/abs/1803.03922
>>
>> Sniff, still passed the deadline Q1 2026 for
>> my GigaLIPS Prolog. There were so many other
>> improvements , more low hanging fruits to cover.
>>
>> Bye
>>
>> P.S.: Wanna rent some GPUs?
>>
>> Cloud GPU Index
>> Compare 2,542 GPU prices across 57 cloud providers
>> https://getdeploying.com/gpus
>>
>> Mild Shock schrieb:
>>> Well its called "artificial" intelligence.
>>> Like "atificial" flowers made from plastic
>>> try to share the look and feel of natural flowers,
>>>
>>> articial intelligence tries to share the
>>> look and feel of natural intelligence.
>>> AI is not really genetic engineering of
>>>
>>> bioforms, right? However, there is a research
>>> frontier sometimes called biocomputing or
>>> synthetic biology AI.
>>>
>>> Kunstblumen
>>> https://www.xxxlutz.ch/kunstblumen-C22C8C1
>>>
>>> The convergence of AI and synthetic biology: the looming deluge
>>> https://www.nature.com/articles/s44385-025-00021-1
>>>
>>> x schrieb:
>>>> On 3/7/26 03:08, Mild Shock wrote:
>>>>> Hi,
>>>>>
>>>>> Resolution of Erd˝os Problem #728
>>>>> We provide a writeup of a resolution of Erd˝os
>>>>> Problem #728; this is the first Erd˝os problem
>>>>> (a problem proposed by Paul Erd˝os which has
>>>>> been collected in the Erd˝os Problems website [3])
>>>>> regarded as fully resolved autonomously by an AI
>>>>> system. The system in question is a combination of
>>>>> GPT-5.2 Pro by OpenAI and Aristotle by Harmonic,
>>>>
>>>> I guess there is something called 'logic' and then
>>>> there is something called 'semantics'.
>>>>
>>>> Does it matter if words have meaning?  If the
>>>> answer is no - then of course you can generate
>>>> the look and feel of meaning through 'AI'.
>>>>
>>>>
>>>
>>
> 

Back to sci.physics | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Re: AI solves probl;em Knuth was/is working on! Mild Shock <janburse@fastmail.fm> - 2026-03-04 08:29 +0100
  Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728 (Re: AI solves probl;em Knuth was/is working on!) Mild Shock <janburse@fastmail.fm> - 2026-03-07 11:58 +0100
    Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-07 12:08 +0100
      Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:21 -0800
        Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:36 -0800
          Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:00 +0100
            Re: Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:19 +0100
              Amazing Visual Perception, even for ASCII Input [GPT 5.3] (Was: Only, three decades in software engineering?) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:34 +0100
                Visual Perception helps reading Matrices, Fractions, etc.. (Re: Amazing Visual Perception, even for ASCII Input [GPT 5.3]) Mild Shock <janburse@fastmail.fm> - 2026-03-08 20:21 +0100
      Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) x <x@x.net> - 2026-03-08 19:10 -0700
        Biobrain cannot digest "Artificial" in AI (Was: Aristotle: The Era of Vibe Proving is Here) Mild Shock <janburse@fastmail.fm> - 2026-03-09 11:21 +0100
          Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-04-04 14:10 +0200
            Buddos Waterloo: Checkpoint McCune (Re: Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:20 +0200
              Could ISAMORE anti-unification help? (Re: Buddos Waterloo: Checkpoint McCune) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:48 +0200

csiph-web