Agreed. I came at this a someone doing practical work with a CAS, frustrated with how stupid it seemed, but you're right that I should have dropped the CAS references and gone for the juggular -- particularly given my management of the Laws of Form mailing list arising from my association with The Boundary Institute's purpose (which Faggin funded).
Treating "a full-on Automated Theorem Proving system" as a Go (or Chess, or...) player makes sense to me. Does it to you? On Wed, Mar 24, 2021 at 1:01 AM Ben Goertzel <[email protected]> wrote: > On Tue, Mar 23, 2021 at 9:53 PM James Bowery <[email protected]> wrote: > > > > I constrained mutations to "algebraic identities" -- which constrains > the paths to the search space. So the evolutionary program synthesis is > more along the lines of a computer algebra system searching for a proof. > > If the algebraic identities are a broad enough class to work for > general program search, then they're going to map by Curry-Howard type > correspondences into logical co-implications in a pretty general > quantifier logic (or something similar) ... meaning this is going to > be more along the lines of a full-on Automated Theorem Proving system > than a computer algebra system > > -- ben ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/Tf8bb7754cbb517a4-Maafebe7348c8ade3026ffc28 Delivery options: https://agi.topicbox.com/groups/agi/subscription
