Objetivo:

Escriba un programa o función completa que tome una fórmula en lógica proposicional (de aquí en adelante referida como expresión o expresión lógica ) y genere esa fórmula en forma conjuntiva normal . Hay dos constantes, ⊤y ⊥que representa verdadero y falso, un operador unario ¬que representa la negación, y operadores binarios ⇒, ⇔, ∧, y ∨que representa implicación, equivalencia, conjunción, y la disyunción, respectivamente, que obedecen a todas las operaciones lógicas habituales ( la ley de DeMorgan , eliminación doble negación , etc.)

La forma normal conjuntiva se define de la siguiente manera:

1. Cualquier expresión atómica (incluyendo ⊤y ⊥) está en forma conjuntiva normal.
2. La negación de cualquier expresión previamente construida está en forma conjuntiva normal.
3. La disyunción de cualquiera de las dos expresiones construidas previamente está en forma conjuntiva normal.
4. La conjunción de dos expresiones construidas previamente está en forma conjuntiva normal.
5. Cualquier otra expresión no está en forma conjuntiva normal.

Cualquier expresión lógica se puede convertir (de forma no exclusiva) en una expresión lógicamente equivalente en forma conjuntiva normal (consulte este algoritmo ). No necesita usar ese algoritmo particular.

Entrada:

Puede tomar la entrada en cualquier formato conveniente; por ejemplo, una expresión lógica simbólica (si su idioma lo admite), una cadena, alguna otra estructura de datos. No necesita usar los mismos símbolos para los operadores verdadero, falso y lógico que yo hago aquí, pero su elección debe ser coherente y debe explicar sus elecciones en su respuesta si no está claro. No puede aceptar ninguna otra entrada ni codificar ninguna información adicional en su formato de entrada. Debería tener alguna forma de expresar un número arbitrario de expresiones atómicas; ej. enteros, caracteres, cadenas, etc.

Salida:

La fórmula en forma conjuntiva normal, nuevamente en cualquier formato conveniente. No necesita estar en el mismo formato que su entrada, pero debe explicar si hay alguna diferencia.

Casos de prueba:

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

Notas:

1. Si la expresión de entrada es una tautología, ⊤sería una salida válida. Del mismo modo, si la expresión de entrada es una contradicción, ⊥sería una salida válida.
2. Los formatos de entrada y salida deben tener un orden de operaciones bien definido capaz de expresar todas las expresiones lógicas posibles. Es posible que necesite paréntesis de algún tipo.
3. Puede utilizar cualquier opción bien definida de notación de infijo, prefijo o postfix para las operaciones lógicas. Si su elección difiere del estándar (la negación es el prefijo, el resto es infijo), explique eso en su respuesta.
4. La forma normal conjuntiva no es única en general (ni siquiera reordena). Solo necesita generar un formulario válido.
5. Independientemente de cómo represente las expresiones atómicas, deben ser distintas de las constantes lógicas, los operadores y los símbolos de agrupación (si los tiene).
6. Se permiten los elementos integrados que calculan la forma normal conjuntiva.
7. Las lagunas estándar están prohibidas.
8. Este es el código de golf ; la respuesta más corta (en bytes) gana.

Máximo, 4 bytes

pcnf

¡Pruébelo en línea!

Se puede utilizar implies, eq, and, or operadores de implicación, equivalencia, conjuntamente, y la disyunción, respectivamente.

Me vas a odiar ...

Mathematica, 23 bytes

#~BooleanConvert~"CNF"&

La entrada utiliza Truey Falseen lugar de ⊤y ⊥, pero por lo demás se verá muy similar a la notación de la cuestión: todos los personajes ¬, ⇒, ⇔, ∧, y ∨son reconocidos en Mathematica (cuando la entrada de caracteres UTF-8 00AC, F523, 29E6, 2227 , y 2228, respectivamente), y los paréntesis actúan como cabría esperar.

De manera predeterminada, la salida utilizará los símbolos preferidos de Mathematica: por ejemplo, se emitirá el último caso de prueba en (! P || ! Q || R) && (! P || Q || ! R)lugar de ((¬ P) ∨ ((¬ Q) ∨ R)) ∧ ((¬ P) ∨ (Q ∨ (¬ R))). Sin embargo, cambiando la función a

TraditionalForm[#~BooleanConvert~"CNF"]&

hará que la salida se vea bonita y conforme a estos símbolos habituales:

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

El formato de E / S es el siguiente (en orden de precedencia):

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

Ejemplos:

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)))

La función se reescribe trivialmente para producir una forma normal disyuntiva:

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

Se podrían guardar 8 bytes de esta versión si también se me permitiera asumir la precedencia anterior en la salida, lo que eliminaría todos los paréntesis de los ejemplos de salida:

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)))