Propositional logic sure has become a standard notion of our scientifically educated society, maybe as much as the arithmetic systems of integers, rational and real numbers. Boolean operations are standards in many areas of our computerized daily life, digital logic is the mathematical structure behind the computer hardware and information software.
But different to arithmetic systems and other basic data structures like lists, matrices or regular expressions, propositional algebras are not part of the standard tool repertoire of programming languages. This is certainly due to the cost explosion (see e.g. the boolean satisfiability problem) of its default implementation. What we need, is a fast implementation, which allows these structures to be used as basic tools for other programs.
The other problem with propositional logic is its classic algebraization as a (free) boolean algebra, which is only an abstraction of the semantic structure of propositional logic. That way, we loose some of the information. In other words, we need an algebraization that also preserves the syntactic structure of propositional worlds.
I am happy to announce the release of PropLogic, a Haskell package that intents to fix these problems and that might serve as a general and useful tool.
Despite my original intent to write a compact implementation for a pretty compact theory, this distribution is overloaded in an attempt to explain all its aspects. I suppose, the best place to start is A little program for propositional logic and a Brief introduction to PropLogic.
The first of these two tutorials doesn't require prior Haskell knowledge. Any fast implementation of a propositional algebra also provides a fast SAT solver and there is an interest and competition for the quickest solution. I have no idea how my program performs compare to other existing algorithms out there, but I tried to illustrate with some data how good it does the job. (I must admit however, that my "fast" program has its limits, too.)
The thing seems to work properly as it is, but I would still like to do some polishing and upload it to Hackage, soon. It would be very nice to get a boost from the comments and reactions of the Haskell community.
I would not describe this as a "Brief" introduction! It is quite thorough, and quite an enjoyable read, too :)
ReplyDeleteOne comment, there is seemingly little reference to fairly standard Haskell packages. Would something like Data.Sequence not be a good fit for your Costack needs? The presentation in parts, such as that one, feels unnecessarily removed from mainstream Haskell programming. The way you provide such a thorough harness for driving the code from the command line is a rarity. Most examples would focus on GHCi interactions rather than CLI interactions.
It will be very nice to see this on Hackage.
Typo in "A little program..." that I stared at trying to reconcile for a while, "Alltogether, there are three prime factors of [[x + -z] + [y * z]], namely [x * y], [x * -z] and [y * z]."
Hello Anonymous, thank you very much for your comment and the time you took.
ReplyDelete(1.) Yes, you are right, "Brief" it was when I started it, now it's a lie. (Don't wan't to bother changing it, though. Leave it as a trap to catch readers. ;-)
(2.) Thank you for your pointer to Data.Sequence. And yes, you are certainly right, again. I often get carried away in explaining the obvious. Instead, I should really get more familiar with the mainstream and rely on it.
(3.) And you are right, once more: "[[x + -z] + [y * z]]" had to be "[[x * -z] + [y * z]]". I changed it in the online version.
This is very nice. I do have some suggestions for the packaginging. First, the Main module is exported to the library, which is probably not what you meant to do. The TextDisplay module is not, which means you can't use display as shown in the examples. I also think the modules should be moved into the standard Haskell heirarchy - maybe under Data.PropLogic?
ReplyDeleteIn order to correct my previous comment: item (1.) was a dull joke and I did deleted the adjective "Brief" in the "Brief introduction to PropLogic" title. That's better.
ReplyDeleteDear David Fox!
ReplyDeleteI appreciate your comment. This is good advise.
There are some issues I don't fully understand with the whole packaging thing in Haskell distributions.
I while ago, I wrote a cabal file
http://www.bucephalus.org/PropLogic/PropLogic.cabal
But this is obviously incomplete.
I am going to import PropLogic to a darcs repository at http://src.seereason.com/PropLogic and apply patches to fix it up a little bit. Then you can take them if you like them.
ReplyDeleteDear David Fox!
ReplyDeleteThank you very much, again.
On a Haskell user group meeting yesterday I got some more very good advice about the packaging. I intend to wrap things up, soon, and then upload it to Hackage.
What I don't understand, however, is the mutation of the structure when you moved it to src.seereason.com. You split the modules with "PropLogic" in their names (like PropLogicCore and DefaultPropLogic) and moved them into subdirectories, while other modules like Olist or Costack stayed in the main directory. This is not reflecting the structure and looks very strange to me.
Yesterday, I got the advise to integrate the package into the Haskell hierachy under the data subdirectory. I think I'll do that.
Well, I'm not really an expert, I may have misunderstood the intent of your code, or failed to think it through. At this point I'm only using the PropForm datatype.
ReplyDeleteInteresting article, added his blog to Favorites
ReplyDeleteSpeaking of the PropForm datatype, I would suggest that it is unfortunate that CJ [a, b] is not EQ to CJ [b, a] - it might be better to use sets for the arguments of commuative operators rather than lists.
ReplyDeleteHi,
ReplyDeleteAbout the SAT solving part. I want to check if I understand the documentation correctly. Does the following command
./PropLogic primForm "[[-1,2,3],[1,2,3],[-1,2,-3],[-1,-2,3],[-1,-2,3],[-1,2,3]]"
that results in
[[-1,2],[-1,3],[2,3]]
mean that all three disjunction pairs in the result contain a valid truth value assignment to solve the problem? Isn't finding all possible ways to satisfy the SAT problem much slower than just finding one solution? Or is there some other way for just finding "the first" solution to the satisfiability problem?
Please, what is the name of the author of PropLogic?
ReplyDeleteNice post. Keep updating Artificial Intelligence Online Training
ReplyDelete