Messing with skolemization

Posted on 2014 03 21 by phimuemue

In predicate logic, skolemization is a central method to manipulate logic formulas. Since we had to do some homework on those formulas, and I always mixed up the parentheses, I decided to have it done by the computer. So, below you'll find an implementation of skolemization in Haskell. It takes a formula specified in (admittedly clumsy) haskell data type syntax, and

I can't guarantee that it is working correctly, but at least for my example, it worked out quite well. You can get the source here.

Note that this implementation is not optimal at all. There are several unelegant and inefficient passages, which is most due to the fact that I didn't do very much in Haskell in the past. However, I always liked the way one can express and transform some kind of algebraic formulas in this programming language.