[…] A Prolog Theorem Prover simplifying Logic, by using Multiple Forms The strategy of this Prolog program („mflogic.exe“, which you can download) is essentially the same as the strategy of a (human) theorem-prover, who knows the Axioms of Multiple Forms: As much as possible, all logic formulae are progressively reduced, by cancelling out „Outer Parts“ if these are also found in „Inner Parts“ of expressions (using Axiom 3). They are also reduced by “ the All” (=One) „absorbing anything“ that “exists outside itself” (using Axom 1), or (finally) reduced by pairs of identical forms “ collapsing” when they apply to each other, “distinguishing each other” (XOR-wise, by Axiom 2).
The Prolog program „includes some extensive automatic comments, sprinkled over the derivation steps, so it can become an educational tool for learning Multiple Form Logic™.“
Find a screenshot here:
George, a.k.a. Omadeon,
„wrote it recently, coming back to Multiple Form Logic™ after a long period of absence from this field, and it is still Version 1. Future versions planned may include graphic representations of Multiple Form simplifications, which are quite spectacular, even on paper, like watching an avalanche of ‚bubbles‘ breaking and re-organising themselves.“
By the way, what are traditional Propositional Logic formulae? The Prolog program translates them into Multiple Form Logic™, and then uses repeatedly the Three Fundamental Axioms of Multiple Form Logic as re-write rules, until the resulting expression is irreducible. (You can either pick a formula from a library, or write your own). Then, the result is converted back into Propositional Calculus. Multiple Form Logic™ is supposed to do better than just ‚prove theorems‘ to be ‚true‘ or ‚false‘; but actually „optimizes logic expressions, regardless of whether or not they are reducible to true or false.“