Problem solving in metalogic programming