phimuemue

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.

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.

The following is a very simple unification algorithm in Haskell.

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

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