Recently I sent an e-mail to the «Pile System» site, proposing that their system can be used in more efficient automatic theorem provers for «Multiple Form Logic«. Mr. Ralf Barkow, a Pile researcher, has been exploring intriguing relationships between «Multiple Form Logic» and «Pile«, about a year ago. E.g.
I have not heard from them yet, but fortunately (if they are too busy to reply) their «Pile development system» can be downloaded freely (even though commercial use is prohibited by their patents). So I downloaded it a couple of days ago.
I discovered the existence of the «Pile system» fairly recently. I’d recommend it -as creative reading- to anyone seriously interested in Computer Science innovations. Here are some links I collected about «Pile«, as public bookmarks:
My own work in «Multiple Form Logic» is an enhancement and generalisation of George Spencer Brown‘s «Laws of Form«. Here are some links about Spencer-Brown (GSB) and «Laws of Form» (LoF), as public bookmarks:
There are interesting reasons why Multiple Form Logic inference engines can benefit by using Pile‘s revolutionary data-structures inside them: Most computation in Multiple Form Logic theorem provers consists of sub-tree identifications inside tree-like expressions, so that Axiom 3 of MF Logic can be applied repeatedly (for term re-writing). This axiom states that «What is outside a term can be cancelled-out inside it«, where «inside» and «outside» are both «topological» and -somewhat- «metaphysical» or «ontological»:
This «axiom of perception», interpreted philosophically, states that «What is real we may imagine, but we don’t need to imagine what is real«. More information about Multiple Form Logic (and related topics) is now available as public bookmarks:
The Pile system «relationist» approach to data, under the principle of reversible relation-formation, can be used to build Multiple Form Logic structures that are immediately simplifiable without even searching, since sub-expressions (under Pile principles) are already immediately accessible.