Solving sudoku like puzzle with .NET

[condonethis]

What does it do ?

http://en.wikipedia.org/wiki/Twelf

It is a language for mathematic problem solving. Although the method used to obtain the answer for the issue is great, it is nothing more than brute force. Twelf will allow you to problem solve using strategy and deduction, whereas this vb solution is achieved by sheer chance and probability. Twelf can solve a problem in milliseconds that takes minutes in VB.Net

cell : type.
1 : cell.
2 : cell.
3 : cell.
4 : cell.
5 : cell.
6 : cell.
7 : cell.
8 : cell.
9 : cell.

nat : type.
z : nat.
s : nat -> nat. %prefix 5 s.
nine = s s s  s s s  s s s z.

cells : nat -> type.
//  : cell -> cells N -> cells (s N).
%infix right 5 //.
nil : cells z.

cellss : nat -> type.
///  : cells nine -> cellss N -> cellss (s N).
%infix right 4 ///.
nill : cellss z.

remove : cells (s N) -> cell -> cells N -> type.
%mode remove +L +C -L'.

rem-hit  : remove (X // C) X C.
 okay that we can also skip this one
rem-miss : remove (X // C) Y (X // C')
        <- remove C Y C'.

%worlds () (remove _ _ _).
%terminates D (remove D _ _).

nodups : cells X -> cells Y -> type.
%mode nodups +OK +L.

nd-nil  : nodups _ nil.
nd-hit  : nodups OK (X // C)
       <- remove OK X OK'
       <- nodups OK' C.

%worlds () (nodups _ _).
%terminates D (nodups _ D).

 valid if there are no duplicates
allcells = 1 // 2 // 3 //
           4 // 5 // 6 //
           7 // 8 // 9 // nil.

unitok : cells nine -> type.

uo : unitok C
  <- nodups allcells C.

 the nine rows
%abbrev board = cellss nine.

 extract three boxes from three rows
boxes : cells nine -> cells nine -> cells nine ->
        cells nine -> cells nine -> cells nine -> type.
%mode boxes +A +B +C -A' -B' -C'.

b : boxes
      (A1 // B1 // C1  //  D1 // E1 // F1  //  G1 // H1 // I1  //  nil)
      (A2 // B2 // C2  //  D2 // E2 // F2  //  G2 // H2 // I2  //  nil)
      (A3 // B3 // C3  //  D3 // E3 // F3  //  G3 // H3 // I3  //  nil)

      (A1 // B1 // C1 //
       A2 // B2 // C2 //
       A3 // B3 // C3 // nil)

      (D1 // E1 // F1 //
       D2 // E2 // F2 //
       D3 // E3 // F3 // nil)

      (G1 // H1 // I1 //
       G2 // H2 // I2 //
       G3 // H3 // I3 // nil).

%worlds () (boxes _ _ _  _ _ _).
%total {} (boxes _ _ _  _ _ _).

 transpose a whole board
transpose : board -> board -> type.
%mode transpose +B -B'.

tr : transpose ((A1 // B1 // C1 // D1 // E1 // F1 // G1 // H1 // I1 // nil) ///
                (A2 // B2 // C2 // D2 // E2 // F2 // G2 // H2 // I2 // nil) ///
                (A3 // B3 // C3 // D3 // E3 // F3 // G3 // H3 // I3 // nil) ///
                (A4 // B4 // C4 // D4 // E4 // F4 // G4 // H4 // I4 // nil) ///
                (A5 // B5 // C5 // D5 // E5 // F5 // G5 // H5 // I5 // nil) ///
                (A6 // B6 // C6 // D6 // E6 // F6 // G6 // H6 // I6 // nil) ///
                (A7 // B7 // C7 // D7 // E7 // F7 // G7 // H7 // I7 // nil) ///
                (A8 // B8 // C8 // D8 // E8 // F8 // G8 // H8 // I8 // nil) ///
                (A9 // B9 // C9 // D9 // E9 // F9 // G9 // H9 // I9 // nil) /// nill)

               ((A1 // A2 // A3 // A4 // A5 // A6 // A7 // A8 // A9 // nil) ///
                (B1 // B2 // B3 // B4 // B5 // B6 // B7 // B8 // B9 // nil) ///
                (C1 // C2 // C3 // C4 // C5 // C6 // C7 // C8 // C9 // nil) ///
                (D1 // D2 // D3 // D4 // D5 // D6 // D7 // D8 // D9 // nil) ///
                (E1 // E2 // E3 // E4 // E5 // E6 // E7 // E8 // E9 // nil) ///
                (F1 // F2 // F3 // F4 // F5 // F6 // F7 // F8 // F9 // nil) ///
                (G1 // G2 // G3 // G4 // G5 // G6 // G7 // G8 // G9 // nil) ///
                (H1 // H2 // H3 // H4 // H5 // H6 // H7 // H8 // H9 // nil) ///
                (I1 // I2 // I3 // I4 // I5 // I6 // I7 // I8 // I9 // nil) /// nill).
%worlds () (transpose _ _).
%total {} (transpose C _).

boardok : board -> type.

bo : boardok
     (A /// B /// C /// D /// E /// F /// G /// H /// I /// nill)
 rows
  <- unitok A <- unitok B <- unitok C
  <- unitok D <- unitok E <- unitok F
  <- unitok G <- unitok H <- unitok I
 boxes
  <- boxes A B C  Ab Bb Cb
  <- unitok Ab <- unitok Bb <- unitok Cb
  <- boxes D E F  Db Eb Fb
  <- unitok Da <- unitok Ea <- unitok Fa
  <- boxes G H I  Gb Hb Ib
  <- unitok Gb <- unitok Hb <- unitok Ib
 cols
  <- transpose (A  /// B  /// C  /// D  /// E  /// F  /// G  /// H  /// I  /// nill)
               (At /// Bt /// Ct /// Dt /// Et /// Ft /// Gt /// Ht /// It /// nill)
  <- unitok At <- unitok Bt <- unitok Ct
  <- unitok Dt <- unitok Et <- unitok Ft
  <- unitok Gt <- unitok Ht <- unitok It.

%solve _ : boardok
(
(8 // 2 // 6  //  7 // 1 // 4  //  9 // 5 // 3  // nil) ///
(3 // 4 // 5  //  8 // 6 // 9  //  2 // 1 // 7  // nil) ///
(9 // 7 // 1  //  2 // 5 // 3  //  4 // 8 // 6  // nil) ///

(1 // 6 // 3  //  9 // 2 // 5  //  7 // 4 // 8  // nil) ///
(5 // 9 // 4  //  6 // 7 // 8  //  1 // 3 // 2  // nil) ///
(2 // 8 // 7  //  3 // 4 // 1  //  5 // 6 // 9  // nil) ///

(7 // 5 // 9  //  4 // 3 // 6  //  8 // 2 // 1  // nil) ///
(4 // 3 // 2  //  1 // 8 // 7  //  6 // 9 // 5  // nil) ///
(6 // 1 // 8  //  5 // 9 // 2  //  3 // 7 // 4  // nil) /// nill).

%solve _ : boardok
(
(8 // 2 // 6  //  7 // 1 // 4  //  9 // 5 // 3 // nil) ///
(3 // 4 // 5  //  8 // 6 // 9  //  2 // 1 // 7  // nil) ///
(9 // 7 // 1  //  2 // 5 // 3  //  4 // 8 // 6  // nil) ///

(1 // 6 // 3  //  _ // 2 // 5  //  7 // 4 // 8  // nil) ///
(5 // 9 // 4  //  _ // 7 // 8  //  1 // 3 // 2  // nil) ///
(2 // 8 // 7  //  _ // _ // 1  //  5 // 6 // 9  // nil) ///

(7 // 5 // 9  //  4 // 3 // 6  //  8 // 2 // 1  // nil) ///
(4 // 3 // 2  //  1 // 8 // 7  //  6 // 9 // 5  // nil) ///
(6 // 1 // 8  //  5 // 9 // 2  //  3 // 7 // 4  // nil) /// nill).

-http://twelf.org/wiki/Sudoku