# Messing with skolemization

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. 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.