Objetivo:

Escrever um programa completo ou função que tem uma fórmula em lógica proposicional (daqui em diante referido como uma expressão lógica ou expressão ) e saídas que a fórmula na forma normal conjuntiva . Há duas constantes, ⊤e ⊥que representa o verdadeiro eo falso, um operador unário ¬representando negação e operadores binários ⇒, ⇔, ∧, e ∨representando implicação, equivalência, conjunção e disjunção, respectivamente, que obedecer todas as operações lógicas habituais ( lei de DeMorgan , eliminação dupla negação etc.).

A forma normal conjuntiva é definida da seguinte forma:

1. Qualquer expressão atômica (incluindo ⊤e ⊥) está na forma conjuntiva normal.
2. A negação de qualquer expressão construída anteriormente está na forma conjuntiva normal.
3. A disjunção de quaisquer duas expressões construídas anteriormente está na forma conjuntiva normal.
4. A conjunção de quaisquer duas expressões construídas anteriormente está na forma normal conjuntiva.
5. Qualquer outra expressão não está na forma normal conjuntiva.

Qualquer expressão lógica pode ser convertida (de maneira não exclusiva) em uma expressão logicamente equivalente na forma normal conjuntiva (consulte este algoritmo ). Você não precisa usar esse algoritmo específico.

Entrada:

Você pode receber informações em qualquer formato conveniente; por exemplo, uma expressão lógica simbólica (se o seu idioma suportar), uma string, alguma outra estrutura de dados. Você não precisa usar os mesmos símbolos para operadores verdadeiros, falsos e lógicos que eu faço aqui, mas sua escolha deve ser consistente e você deve explicar suas escolhas em sua resposta, se não estiver claro. Você não pode aceitar nenhuma outra entrada ou codificar nenhuma informação adicional em seu formato de entrada. Você deve ter alguma maneira de expressar um número arbitrário de expressões atômicas; por exemplo, números inteiros, caracteres, strings, etc.

Resultado:

A fórmula na forma normal conjuntiva, novamente em qualquer formato conveniente. Ele não precisa estar no mesmo formato da sua entrada, mas você deve explicar se há alguma diferença.

Casos de teste:

P ∧ (P ⇒ R) -> P ∧ R
P ⇔ (¬ P) -> ⊥
(¬ P) ∨ (Q ⇔ (P ∧ R)) -> ((¬ P) ∨ ((¬ Q) ∨ R)) ∧ ((¬ P) ∨ (Q ∨ (¬ R)))

Notas:

1. Se a expressão de entrada for uma tautologia, ⊤seria uma saída válida. Da mesma forma, se a expressão de entrada for uma contradição, ⊥seria uma saída válida.
2. Os formatos de entrada e saída devem ter uma ordem de operações bem definida, capaz de expressar todas as expressões lógicas possíveis. Você pode precisar de parênteses de algum tipo.
3. Você pode usar qualquer opção bem definida de notação de infixo, prefixo ou postfix para as operações lógicas. Se sua escolha for diferente do padrão (negação é prefixo, o restante é infixo), explique-o na sua resposta.
4. A forma normal conjuntiva não é única em geral (nem mesmo reordenando). Você só precisa gerar um formulário válido.
5. Entretanto, como você representa expressões atômicas, elas devem ser distintas das constantes lógicas, operadores e símbolos de agrupamento (se você os tiver).
6. São permitidos embutidos que calculam a forma normal conjuntiva.
7. As brechas padrão são proibidas.
8. Isso é código-golfe ; a resposta mais curta (em bytes) vence.

Máximos, 4 bytes

pcnf

Experimente Online!

Você pode usar implies, eq, and, or operadores de implicação, equivalência, conjunção e disjunção respectivamente.

Você vai me odiar ....

Mathematica, 23 bytes

#~BooleanConvert~"CNF"&

A entrada será usar Truee False, em vez de ⊤e ⊥, mas caso contrário será muito similar à notação da questão: todos os personagens ¬, ⇒, ⇔, ∧, e ∨são reconhecidos no Mathematica (quando a entrada com caracteres UTF-8 00AC, F523, 29E6, 2227 , e 2228, respectivamente), e os parênteses agem conforme o esperado.

Por padrão, a saída usará os símbolos preferidos do Mathematica: por exemplo, o último caso de teste será exibido em (! P || ! Q || R) && (! P || Q || ! R)vez de ((¬ P) ∨ ((¬ Q) ∨ R)) ∧ ((¬ P) ∨ (Q ∨ (¬ R))). No entanto, alterar a função para

TraditionalForm[#~BooleanConvert~"CNF"]&

fará com que a saída fique bonita e em conformidade com estes símbolos comuns:

JavaScript (ES6), 127 bytes

f=(s,t='',p=s.match(/[A-Z]/),r=RegExp(p,'g'))=>p?'('+f(s.replace(r,1),t+'|'+p)+')&('+f(s.replace(r,0),t+'|!'+p)+')':eval(s)?1:0+t

O formato de E / S é o seguinte (em ordem de precedência):

• (: (
• ): )
• ⊤: 1
• ⊥: 0
• ¬: !
• ⇒: <=
• ⇔: ==
• ∧: &
• ∨: |

Exemplos:

P&(P<=R) -> ((1)&(0|P|!R))&((0|!P|R)&(0|!P|!R))
P==(!P) -> (0|P)&(0|!P)
(!P)|(Q==(P&R)) -> (((1)&(0|P|Q|!R))&((0|P|!Q|R)&(1)))&(((1)&(1))&((1)&(1)))

A função é reescrita trivialmente para produzir uma forma normal disjuntiva:

f=(s,t='',p=s.match(/[A-Z]/),r=RegExp(p,'g'))=>p?'('f(s.replace(r,1),t+'&'+p)+')|('+f(s.replace(r,0),t+'&!'+p)+')':eval(s)?1+t:0

8 bytes poderiam ser salvos nesta versão se eu também tivesse permissão para assumir a precedência acima na saída, o que removeria todos os parênteses dos exemplos de saída:

P&(P<=R) -> ((1&P&R)|(0))|((0)|(0))
P==(!P) -> (0)|(0)
(!P)|(Q==(P&R)) -> (((1&P&Q&R)|(0))|((0)|(1&P&!Q&!R)))|(((1&!P&Q&R)|(1&!P&Q&!R))|((1&!P&!Q&R)|(1&!P&!Q&!R)))