Adicionando a função "sentence" e a função "table".

[paulodt]

A função "sentence" recebe a lista de valores, referente ao tabuleiro do sudoku, e retorna a sentença a ser provada. Já a função "table" faz o caminho inverso, ou seja, recebe uma lista de elementos da classe "formula", por exemplo, (<[TRUE] S123> <[TRUE] S212>), e retorna o tabuleiro referente a tal lista.

[arademaker]

A func big-and não é necessária:

tableaux-test> (reduce (lambda (a b) `(and ,a ,b)) `(a b c d e f))
(and (and (and (and (and a b) c) d) e) f)
tableaux-test> (cons 'and `(a b c d e))
(and a b c d e)

A func sudoku ficou sobrando? Os parâmetros *sudoku-1* e `sudoku-2`` também? Acho que isto tudo engloba o issue sobre organizar as entradas e saída de sudoku.

Em Lisp, evitamos o underscore dado que podemos usar hífen. Vide http://google.github.io/styleguide/lispguide.xml como referência mas principalmente os outros exemplos de nomes no projeto.

Precisamos de exemplos na forma de testes. Aceitei mas precisamos melhorar.

[paulodt]

Os parâmetros foram criados apenas para testes. A função sudoku, pelo que vejo, tem o mesmo efeito da função sentence, mas cria um grande array de dimensão (9,9), e a minha cria uma lista apenas, de 81 elementos.

[paulodt]

Poderíamos optar pela função sentence ao invés da função sudoku?

[arademaker]

tanto faz para mim, precisamos apenas decidir, como projeto, não precisamos de duas soluções para a mesma coisa.