## Category: computer science

### A very nice proof of existence

We consider a propositional logic formula in conjunctive normal form, containing clauses, where each clause has exactly k (distinct) variables. We prove that this formula is satisfiable.

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

### A quick and dirty unification algorithm

The following is a very simple unification algorithm in Haskell.

### A seemingly simple problem proven hard

Consider the following problem: You are celebrating a festival and want to invite guests. The only problem is the following: You want to distribute all guests in a single row, but you can only place to guests next to each other if they get along with each other. The question is if there’s an efficient [...]

### Height of an AVL-tree

I came across the following question lately: Show that the height of an AVL-tree is .