A.I. programming in Prolog and Assembler

October 14, 2007

DreamProver: A visual theorem prover for “Multiple Form Logic” (etc.) in LPA Win-Prolog 4.6

Chart showing the stages in the software relea...Image via Wikipedia

Visual DreamProver 1.0 is a new theorem-proving program, developed in LPA Win-Prolog 4.6, with multi-coloured graphics displays of (potentially unlimited) Logic expressions, theorem proofs and deductions in Multiple Form Logic, in the primary algebra of “Laws of Form“, in Boolean Algebra and in a variety of other logic systems (to a large extent used-defined). Here is an animated GIF slide-show of DreamProver’s visual display. It offers unlimited control of size, colour, shape and content for all Logic Expressions and all theorem proofs:

dreamprover430x.gif

(Click on this image for a better quality animated GIF, of size 450Kb)

Although DreamProver is still at the “alpha stage“, I decided to publish a preliminary first report about its features and capabilities, to a large extent already working, to a lesser extent requiring minor debugging and final extensions, before release. I am also doing this for the benefit (and amusement) of a friendly innovative company: “Logic Programming Associates Ltd”, where I worked for a short pleasant period of a few weeks, some years ago (in 2001). LPA are the creators of the LPA Win-Prolog compiler. I hope that LPA continues a long tradition of innovative success through the latest version of their compiler, which also has MIDI (music) programming capabilities (featured in a recent posting, here).

I am also… officially requesting, after the release of DreamProver (and the ensuing free promotion of LPA’s amazing compiler) a small… personal favour: -A legitimate free copy of their newest LPA Win-Prolog 4.7 compiler! 🙂 (as my license for using version 4.6 ends on the last day of 2007).

DreamProver is particularly suited for the display of so-called “Boundary Logic Systems” (first created by George Spencer Brown in “Laws of Form” and then extended by various people in various ways – including my own “Multiple Form Logic” system). However, its (almost unlimited) potential allows the display of many other logic systems, including Parse-Trees of used-defined grammars, since both the shapes and the data-structures they represent can be redefined “on the fly”. In the display shown above, only a small example of a logic expression is used, mainly to demonstrate graphics capabilities. However, if -for example- the Grammar of a subset of English is used, instead of a Logic Expression, the ensuing graphic display of coloured shapes resembles a tree which is symmetric with respect to a “horizon” line in the middle.

The data-structure for this unusual kind of tree-representation is relatively simple, straight-forward and documented (in the final release of DreamProver). It is separate from the internal Logic representation but related to it through specific user-defined rules: Both the “productions” and the “leaves” of such a grammar tree are user-defined in shape and content. The only difference between other kinds of systems and those built-in (as regards the current first version of DreamProver) is that the other systems do not include internal Proof Algorithms and automated deductions, and can only be fed from the results of such processes (through external third-party software). Before final release it is hoped that the input-expressions in other systems are expressed in standard XML, so as to make the software useful to almost any researcher or developer, in any topic that includes parsed tree-expressions. The ultimate goal is also to develop a kind of Universal DreamProver library, available under a professional license to developers for a small fee (that might help sustain this work and pay for the effort of future upgrades). However, the current version of DreamProver is likely to appear as Open Source in the near future. Keep in touch!

Zemanta Pixie

Advertisements

22 Comments »

  1. […] unknown wrote an interesting post today!.Here’s a quick excerptVisual DreamProver 1.0 is a new theorem-proving program, developed in LPA Win-Prolog 4.6, with multi-coloured graphics displays of (potentially unlimited) Logic expressions, theorem proofs and deductions in Multiple Form Logic, … […]

    Pingback by GadgetGadget.info - Gadgets on the web » DreamProver: A visual theorem prover for “Multiple Form Logic … — October 15, 2007 @ 12:47 am

  2. I would like to take a closer look to prolog.

    May I suggest that you include the following “Pages” to your blog?

    * Prolog Tools
    * Prolog Talker

    Prolog tools should contain a compact list of usable prolog tools, filtered and prioritized by the blog owners preferences.

    Prolog Talker should contain a quick-start to get in touch with prolog code. A really quick-start, something like e.g. this one for Ruby:

    http://dev.lazaridis.com/lang/browser/ruby/talker.rb
    http://dev.lazaridis.com/lang/browser/ruby/main.rb

    If I can get in touch with code within 15 min (excl. download time), I’ll for sure take a look at it.

    Comment by lazaridis_com — October 15, 2007 @ 8:16 pm

  3. As to the topic:

    I’ve read “Dream P_ow_er” for about 5 minutes, until I realized it’s “Dream Prover”.

    Possibly rename the product to “Pro Theorem” or “Theorem Pro” or “Visual Theorem”. “Theorem Pro” reed fluent within text, try it.

    Let me know when you like to go to open-source. I can assist you with the several steps needed.

    Comment by lazaridis_com — October 15, 2007 @ 8:26 pm

  4. btw: this LPA website needs really a (small but important) restructuring.

    http://www.lpa.co.uk

    Comment by lazaridis_com — October 15, 2007 @ 8:58 pm

  5. First of well, a warm welcome to you, Lazaridis, and my sincere apologies for the accidental temporary “moderation queue” (a default option in WordPress that I forgot till now)…

    Well, these magnificient people (in LPA) whom I know one-by-one quite well, replied almost immediately, and quite positively to my e-mail.

    Within minutes I was awarded with their professional compiler and all the toolboxes as well! I also… played with the new compiler’s MIDI music predicates, fascinating and very easy to understand.

    I _must_ finish all other projects ASAP to start Intelligent Music programming, dear Lazaridis.

    As regards what you wrote, now:
    1)
    “DreamProver” is fine by me, if people mistaken it for “DreamPower” SO MUCH THE BETTER! (hehe) It’s part of what it means anyway, as logic is revealled to be the Power of Dreaming ANYWAY, dear Lazaridis (my 3rd axiom of it, etc). Moreover, “DreamProver” reminds people of “DreamWeaver”, too. (i.e. Subliminal free advertising for both)

    2)
    LPA’s site is always serious and somewhat conservative as most of the clients are serious (sometimes also old) University Professors.
    (although of course, you WOULD find something to criticize, wouldn’t you? hehe)

    3)”Prolog talker” is totally meaningless. Just because you used it, heh? 🙂 Sorry, it sounds like a speech application to me. Probably it’s a good title for SUCH applications anyway (but little else).

    However, the two categories you suggested are correct, I think. There is also more, more, more…
    The topic is vast, and life is short! 🙂

    Comment by omadeon — October 15, 2007 @ 11:00 pm

  6. 1) ““DreamProver” reminds people of “DreamWeaver”, too. (i.e. Subliminal free advertising for both)” – a unique product should have a unique name. The name should be descriptive.

    2) LPA should attract new customers with their product. I was not able to get an overview within minutes. that’s too much.

    http://lazaridis.com/efficiency/website.html

    the site needs at _minimum_ a decent navigation bar. I criticize only where it makes sense (e.g. where I see ability/capability).

    3) You are absolutely right. The page should be called “Quick Start”, and should start with something like “Get in touch with prolog code within 15 minutes, using the free tool .

    The two categories which I’ve suggested are not “correct”. They are _essential_ for such a site.

    Comment by lazaridis_com — October 16, 2007 @ 8:06 am

  7. Well, the name DreamProver is BOTH unique AND descriptive.

    If you disagree, find another one AS unique AND as descriptive.

    And also… as PASSIONATE.
    🙂

    Comment by omadeon — October 16, 2007 @ 10:19 am

  8. “Well, the name DreamProver is BOTH unique AND descriptive.”

    Maybe for you. Most possibly, because for you a “Theorem” is a “Dream”. For other people, a “Dream” is a “Bingo”, a “pretty lady” an “investment plan”.

    Of course, if you do the things for you (that’s the impression you gave me), the name is perfect.

    “If you disagree, find another one AS unique AND as descriptive.”

    cannot, you’re the best name-finder for yourself.

    “And also… as PASSIONATE.”

    ouh! I give up.

    Comment by lazaridis_com — October 16, 2007 @ 10:27 am

  9. My main interested is the prolog Quick Start (e.g. based on a free version of LPA’s toolsets).

    Comment by lazaridis_com — October 16, 2007 @ 10:29 am

  10. You can write to LPA using their support page.

    After Murphy
    There is Lazaridis Law (LL1)
    “If something can be criticised,
    it WILL be criticised”. 🙂

    Comment by omadeon — October 16, 2007 @ 11:51 am

  11. P.S. Going for a swim in the Sea now. Will see what’s going on a couple of hours later, at least.

    Comment by omadeon — October 16, 2007 @ 11:53 am

  12. “You can write to LPA using their support page.”

    I am interested in a quick-start provided by you on this site.

    have a good swim.

    Comment by lazaridis_com — October 16, 2007 @ 12:33 pm

  13. Hey George

    I have been thinking along the same lines for quite some time now. Even worked for BG (at the same time MW worked there). So I would very much like to play with your DreamProver. Is it available for download ?

    Thanx

    Comment by youlian — February 8, 2008 @ 6:14 pm

  14. Hi Youlian,

    Thank you for your interest.
    Well, as I already said, DreamProver’s version is “alpha”, not even beta, i.e. not yet suitable for third party testers.
    There are a few known bugs, as well as a plan to upgrade the strategy mechanism for theorem proofs, using currently available open source theorem provers (unfortunately most of them not written in Prolog).

    To be honest, there are some other (more urgent) projects I am working on (apart from excessive blogging -hehe);
    e.g. Semantic Web work is increasing, leaving little time free to continue DreamProver. If all goes well, however, the few remaining bugs will be removed and DreamProver will probably become a “beta version”, around Easter 2008.

    BTW, What is “BG”, and who is “MW”?

    Best Regards

    Comment by omadeon — February 9, 2008 @ 8:16 am

  15. Mongeese says : I absolutely agree with this !

    Comment by mongeese — May 30, 2008 @ 6:27 am

  16. Unfortunately, the completion date of the final version of “DreamProver” has again been postponed, due to an increasing number of other projects.

    Dreamprover Is my only project which is NOT relevant to any business practically at the moment, has NO deadlines, and the only one who benefits or loses from it is… me.

    Comment by omadeon — May 30, 2008 @ 8:24 am

  17. […] DreamProver: A visual theorem prover for “Multiple Form Logic” (etc.) in LPA Win-Prolog … […]

    Pingback by Multiple Form Logic seems to be compatible with “Pile_Objects” and Erez Elul’s “Pile System” ! « OMADEON — December 14, 2008 @ 7:46 am

  18. […] DreamProver: A visual theorem prover for “Multiple Form Logic” (etc.) in LPA Win-Prolog … […]

    Pingback by The CONSISTENCY of ODYSSEUS ELYTIS-”Genesis” with George SPENCER-BROWN’s ideas in “LAWS of FORM” « OMADEON — December 14, 2008 @ 9:28 am

  19. […] DreamProver: A visual theorem prover for “Multiple Form Logic” (etc.) in LPA Win-Prolog … […]

    Pingback by Η συνάφεια της “Γένεσης” του Ελύτη (Άξιον Εστί) με τις ιδέες του George Spencer-Brown στο βιβλίο του “Laws of Form” « OMADEON — December 14, 2008 @ 9:48 am

  20. […] difficulty of  visual representation; a challenge for Visualisation software; e.g. “DreamProver“  -my own visual theorem prover, totally un-funded, delayed, long overdue; more about […]

    Pingback by Wikipedia’s new references to Multiple Form Logic, etc. « Laws of Form weblog — February 14, 2009 @ 12:17 am

  21. Hi there, I found your blog via Yahoo and google while trying to find free midi music and your post caught my interest.

    Comment by Bryan Higgenbotham — February 7, 2010 @ 12:48 pm

  22. I adore your texts greatly. That is why I would like to use them in my paper, if it’s ok for you. I am interesting in that topic. Please, say YES. I warmly many thanks.

    Comment by Paris Wimberley — June 2, 2011 @ 12:41 pm


RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Create a free website or blog at WordPress.com.

%d bloggers like this: