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

• pushes negations as close to the predicates as possible
• ensures that variable names are unique
• brings quantifiers to front
• eliminates existential quantifiers

I can’t guarantee that it is working correctly, but at least for my example, it worked out quite well.

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.