search

arademaker / krr

Knowledge Representation and Reasoning
3 stars 6 forks source link

Clausal de/para CNF #26

Open bernardorusso opened 9 years ago

bernardorusso commented 9 years ago

Funções de transformação de uma sentença Clausal em CNF

bernardorusso commented 9 years ago

Funções implementadas no pull request

arademaker commented 9 years ago

pull não aceito. ainda pendente.

arademaker commented 9 years ago

Em #31 queremos obter de uma formula CNF que seja um AND de ORs de literais (atômicas ou negação de atômicas). Aqui queremos de uma CNF obter uma lista de clausulas onde cada clausula é uma lista de literais.

Pode ser que seja mais fácil unificar estes dois issues dado que apenas a lista de listas é a saída útil para resolução e talvez obte-la da CNF seja tão ou mais complicado de obte-la diretamente da fórmula de entrada.