Sistema de Hilbert - Automatizar Prueba

StackOverflow https://stackoverflow.com/questions/1581256

Pregunta

Estoy intentando probar la afirmación ~ (a-> ~ b) => a en un Hilbert sistema de estilo . Por desgracia, parece que es imposible llegar a un algoritmo general para encontrar una prueba, pero estoy buscando una estrategia de tipo fuerza bruta. Cualquier ideas sobre cómo atacar este son bienvenidos.

¿Fue útil?

Solución

Si te gusta la "programación" en combinatoria lógica , entonces

  • Puede automáticamente "traducir" algunos problemas de lógica en otro campo:. Probando la igualdad de términos lógicos combinatorios
  • Con una buena práctica de programación funcional, puede resolver que,
  • y después, puede traducir la parte posterior respuesta a una prueba de estilo de Hilbert de su problema de lógica original.

La posibilidad de esta traducción en asegurada por Curry-Howard correspondencia .

Desafortunadamente, la situación es tan simple solamente para un subconjunto de (proposicional) lógica: restringido usando condicionales. La negación es una complicación, no sé nada de eso. Por lo tanto no puedo responder a esta pregunta concreta:

¬ ( α ⊃ ¬ β ) ⊢ α

Sin embargo, en los casos en que la negación no es parte de la pregunta, la traducción automática mencionado (y retrotraducción) puede ser una ayuda, siempre y cuando ya tengas práctica en la programación funcional o lógica combinatoria.

Por supuesto, hay otras ayudas, también, en el que podemos permanecer dentro del ámbito de la lógica:

  • demostrando el problema en algún sistema deductivo más intuitivo (por ejemplo naturales deducción )
  • y después usando metateorema s que proporcionan una posibilidad "compilador": la realización de "alto nivel de" prueba de la deducción natural a la 'máquina de código' del sistema de deducción de estilo de Hilbert. Me refiero, por ejemplo, el teorema de metalógico llamado " deducción teorema ".

En cuanto a los probadores de teoremas, por lo que yo sé, las capacidades de algunos de ellos se extienden de modo que puedan aprovechar la asistencia humana interactiva. P.ej. Coq es tal.

Apéndice

Veamos un ejemplo. Cómo probar α ⊃ α

Hilbert sistema

  • Verum ex quolibet α , β se asume como un esquema de axioma, afirmando que frase α ⊃ β ⊃ α se espera que sea deducible, instanciado para cualquier subsentences α , β
  • regla de la cadena α , β , γ se asume como un axioma esquema, que indica que la oración ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ se espera que sea deducible, instanciado para cualquier subsentences α , β
  • Modus ponens se asume como una regla de inferencia: siempre que α ⊃ β es deducible, y también α es deducible, entonces espera ser justificado inferir que también α ⊃ β es deducible.

Vamos a demostrar el teorema:. α ⊃ α es deducible para cualquier α proposición

Introduzcamos las siguientes notaciones y abreviaturas, el desarrollo de un "cálculo prueba":

Prueba cálculo

  • VEQ α , β : ⊢ α ⊃ β ⊃ α
  • CR α , β , γ : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ
  • MP : Si ⊢ α ⊃ β y ⊢ α , entonces también ⊢ β

Una notación diagrama de árbol:

axioma esquema - Verum ex quolibet:


━━━━━━━━━━━━━━━━━ [ VEQ α , β ]
⊢ α ⊃ β ⊃ α

Aesquema de Xiom - regla de la cadena:


━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR α , β , γ ]
⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

regla de inferencia - modus ponens:


⊢ α ⊃ β ⊢ α
━━━━━━━━━━━━━━━━━━━ [ MP ]
⊢ β


árbol de prueba

Veamos una representación en diagrama de árbol de la prueba:


━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ CR α , α ⊃ α , α ] ━━━━━━━━━━━━━━━ [ VEQ α , α ⊃ α ]
⊢ [ α ⊃ ( α ⊃ α ) ⊃ α ] ⊃ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α ⊢ α ⊃ ( α ⊃ α ) ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━ [ MP ] ━━━━━━━━━━━ [ VEQ α , α ]
⊢ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α ⊢ α ⊃ α ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━ [ MP ]
⊢ α ⊃ α

fórmulas de prueba

(?? Algebraica cálculo)

Veamos un más concisa, incluso representación de la prueba:

( CR α , α ⊃ α , α VEQ α , α ⊃ α ) VEQ α , α : ⊢ α ⊃ α

Por lo tanto, podemos representar el árbol de prueba por una sola fórmula:

  • la bifurcación del árbol (modus ponens) se representa mediante una simple concatenación (paréntesis),
  • y las hojas del árbol son prestados por las abreviaturas de los nombres de axiomas correspondientes.

Es digno de registro torreón sobre la creación de instancias de hormigón, que' se compone tipo aquí con parámetros subindexical.

Como se verá a partir de la serie de los ejemplos a continuación, podemos desarrollar un cálculo prueba , donde axiomas están anotadas como una especie de combinadores de base ponens y modus es anotada como un mero aplicación de sus subproofs "premisa":

Ejemplo 1

VEQ α , β : ⊢ α ⊃ β ⊃ α

entiende como

Verum ex quolibet esquema de axioma instancia con α , β proporciona una prueba de la declaración, que α ⊃ β ⊃ α es deducible.

Ejemplo 2

VEQ α , α : ⊢ α ⊃ α ⊃ α

Verum ex quolibet esquema de axioma instancia con α , α proporciona una prueba de la declaración, que α ⊃ α ⊃ α es deducible.

Ejemplo 3

VEQ α , α ⊃ α : ⊢ α ⊃ ( α ⊃ α ) ⊃ α

entiende como

Verum ex quolibet esquema de axioma instancia con α , α ⊃ α proporciona una prueba de la declaración, que α ⊃ ( α ⊃ α ) ⊃ α es deducible.

Ejemplo 4

CR α , β , γ : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

entiende como

regla de la cadena esquema de axioma instancia con α , β , γ proporciona una prueba para la instrucción, que ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ es deducible.

Ejemplo 5

CR α , α ⊃ α , α : ⊢ [ α ⊃ ( α ⊃ α ) ⊃ α ] ⊃ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α

entiende como

regla de la cadena esquema de axioma instancia con α , α ⊃ α , α proporciona una prueba para la afirmación de que [ α ⊃ ( α ⊃ α ) ⊃ α ] ⊃ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α es deducible.

Ejemplo 6

CR α , α ⊃ α , α VEQ α , α ⊃ α : ⊢ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α

entiende como

Si combinamos CR α , α ⊃ α , α y VEQ α , α ⊃ α entre sí a través modus ponens , entonces tenemos una prueba que confirma la siguiente declaración: ( α ⊃ α ⊃ α ) ⊃ α ⊃ α es deducible.

Ejemplo 7

( CR α , α ⊃ α , α VEQ α , α ⊃ α ) VEQ α , α : ⊢ α ⊃ α

Si combinamos la prueba del compund ( CR α , α ⊃ α , α ) junto con VEQ α , α ⊃ α (a través de modus ponens ), entonces tenemos una prueba más del compund. Esto demuestra la siguiente declaración:. α ⊃ α es deducible

combinatoria lógica

A pesar de todo esto por encima de hecho ha proporcionado una prueba para el teorema de esperar, pero parece muy poco intuitivo. No se puede ver cómo la gente puede "descubrir" la prueba.

Veamos otro campo, donde se investigan problemas similares.

lógica combinatoria sin tipo

lógica combinatoria puede considerarse también como un lenguaje de programación funcional extremadamente minimalista. A pesar de su minimalismo, por completo Turing completo, pero evenmore, uno puede escribir programas muy intuitivo y complejas, incluso en este lenguaje aparentemente ofuscado, de forma modular y reutilizable, con un poco de práctica adquirida en la programación funcional "normal" y algunas ideas algebraicas, .

Adición de tipificación gobierna

lógica combinatoria también ha introducido variantes. Sintaxis se aumenta con tipos, y evenmore, además de reglas de reducción, se añaden reglas también escribir.

Para combinadores de base:

  • K α , β se selecciona como un combinador de base, habitar tipo α → β → α
  • S α , β , γ se selecciona como un combinador de base , tipo habitantes ( α → β → γ ) → ( α → β ) → α → γ .

Typing regla de aplicación:

  • Si X tipo habita α → β y Y habita tipo α , luego X Y habita tipo β .

notaciones y abreviaturas

  • K α , β : α → β → α
  • S α , β , γ : ( α → β → γ ) → ( α → β ) * → α → γ .
  • Si X α → β y Y : α , entonces X Y :. β

Curry-Howard correspondencia

Se puede observar que los "patrones" son isomorfos en el cálculo de la prueba y en esta lógica combinatoria mecanografiado.

  • La Verum ex quolibet axioma de los corresponde cálculo prueba en K combinador de base de la lógica combinatoria
  • La Cadena regla axioma de los corresponde cálculo prueba en S combinador de base de la lógica combinatoria
  • Modus ponens regla de inferencia en el cálculo corresponde a prueba a la "aplicación" operación lógica combinatoria.
  • El "condicional" conectivo ⊃ de corresponde lógicos con el tipo de constructor → de la teoría de tipo (y mecanografiadas lógica combinatoria)

La programación funcional

Pero, ¿qué es la ganancia? ¿Por qué debemos traducir problemas a la lógica combinatoria? Yo, personalmente, resulta a veces útil, porque la programación funcional es una cosa que tiene una gran literatura y se aplica en problemas prácticos. Las personas pueden acostumbrarse a ella, cuando se ven obligados a utilizar en las tareas de programación erveryday ans pracice. Y algunos trucos y consejos de la práctica de la programación funcional se pueden aprovechar muy bien en reducciones de lógica combinatoria. Y si una práctica "transferido" se desarrolla en la lógica combinatoria, a continuación, se puede aprovechar también en la búsqueda de pruebas en el sistema de Hilbert.

Enlaces externos

Enlaces cómo los tipos de programación funcional (cálculo lambda, lógica combinatoria) se puede traducir en pruebas lógicas y teoremas:

Enlaces (o libros) como aprender los métodos y prácticas de programa directamente en la lógica combinatoria:

Otros consejos

El sistema de Hilbert no se utiliza normalmente en demostración automática de teoremas. Es mucho más fácil escribir un programa de ordenador para hacer pruebas usando la deducción natural. Del material de href="http://www.cs.umu.se/~hegner/Courses/TDBB08/V98b/Slides/prophilb.pdf" de un supuesto CS :

  

Algunas preguntas frecuentes es sobre el sistema de Hilbert:   Q: ¿Cómo se sabe cual axioma   esquemas de usar, y que   sustituciones para hacer? Puesto que hay   un número infinito de posibilidades, es   no es posible tratar a todos ellos, incluso en   princple. A: No existe un algoritmo; a   menos nadie sencilla. Más bien, uno tiene   ser inteligente. En matemáticas puras,   esto no es visto como un problema, ya   uno está más preocupado por la   existencia de una prueba. Sin embargo, en   aplicaciones informáticas, uno es   interesado en la automatización de la deducción   proceso, por lo que este es un defecto fatal. los   sistema de Hilbert no se utiliza normalmente en   automatizado de teoremas. Q: Entonces, ¿por qué   hacer atención a la gente acerca de Hilbert   ¿sistema? R: Con el modus ponens como su   regla deductiva sola, proporciona una   modelo aceptable de cómo diseñar los seres humanos   demostraciones matemáticas. Como ya veremos,   métodos que son más susceptibles de   implementación informática producir pruebas   que son menos “humano similares.”

Encontrar pruebas de Hilbert cálculo es muy duro.

Se podría tratar de traducir las pruebas de cálculo secuencial o deducción natural de Hilbert cálculo.

Se puede abordar el problema también por el ajuste ¬ α = α → ⊥. A continuación, podemos adoptar el sistema de estilo de Hilbert como se muestra en el apéndice de una de las respuestas, y que sea clásica mediante la adición de los dos axiomas siguientes constantes, respectivamente:

Ex Falso Quodlibet: E α : ⊥ → α
Consequentia Mirabilis: M α : (¬ α → α) → α

A prueba Sist de ¬ (α → β ¬) → α luego lee como sigue:

  1. α ⊢ α (Identidad)
  2. ⊥ ⊢ β → ⊥ (Ex Falso Quodlibet)
  3. α → ⊥, α ⊢ β → ⊥ (Impl Intro izquierda 1 y 2)
  4. α → ⊥ ⊢ α → (β → ⊥) (Impl Intro derecho 3)
  5. ⊥ ⊢ α (Ex Falso Quodlibet)
  6. (α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (Impl Intro Left 4 y 5)
  7. (α → (β → ⊥)) → ⊥ ⊢ α (consequentia Mirabilis 6)
  8. ⊢ ((α → (β → ⊥)) → ⊥) → α (Impl Intro derecho 7)

A partir de esta prueba consecuente, se puede extraer una expresión lambda. Un posible expresiones lambda para la prueba anterior Sist dice lo siguiente:

λy. (M _ Z. (E (y λx. (E (z x)))))

Esta expresión lambda puede ser convertido en un término de esquí. Un posible plazo SKI para la expresión lambda por encima lee como sigue:

S (K M)) (L2 (L1 (K (L2 (L1 (K I))))))
donde L1 = (S ((S (K S)) ((S (K K)) I)))
y L2 = (S (K (S (K E))))

Esto le da a las siguientes pruebas de estilo de Hilbert:

Lema 1: Una forma de la regla de la cadena se debilitó:
1: ((A → B) → ((C → A) → (C → B))) → (((A → B) → (C → A)) → ((A → B) → (C → B ))) [cadena]
2: ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) → (((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B)))) [cadena]
3: ((C → (A → B)) → ((C → A) → (C → B))) → ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) [Verum Ex]
4: (C → (A → B)) → ((C → A) → (C → B)) [Cadena]
5: (A → B) → ((C → (A → B)) → ((C → A) → (C → B))) [MP 3, 4]
6: ((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B))) [MP 2, 5]
7: ((A → B) → ((A → B) → (C → (A → B)))) → (((A → B) → (A → B)) → ((A → B) → (C → (A → B)))) [cadena]
8: ((A → B) → (C → (A → B))) → ((A → B) → ((A → B) → (C → (A → B)))) [Verum Ex] < br> 9: (A → B) → (C → (A → B)) [Verum Ex]
10: (A → B) → ((A → B) → (C → (A → B))) [MP 8, 9]
11: ((A → B) → (A → B)) → ((A → B) → (C → (A → B))) [MP 7, 10]
12: (A → B) → (A → B) [Identidad]
13: (A → B) → (C → (A → B)) [MP 11, 12]
14: (A → B) → ((C → A) → (C → B)) [MP 6, 13]
15: ((A → B) → (C → A)) → ((A → B) → (C → B)) [MP 1, 14]

Lema 2: Una forma de Ex Falso debilitó:
1: (A → ((B → ⊥) → (B → C))) → ((A → (B → ⊥)) → (A → (B → C))) [Cadena]
2: ((B → ⊥) → (B → C)) → (A → ((B → ⊥) → (B → C))) [Verum Ex]
3: (B → (⊥ → C)) → ((B → ⊥) → (B → C)) [Cadena]
4: (⊥ → C) → (B → (⊥ → C)) [Verum Ex]
5: ⊥ → C [Ex Falso]
6: B → (⊥ → C) [MP 4, 5]
7: (B → ⊥) → (B → C) [MP 3, 6]
8: A → ((B → ⊥) → (B → C)) [MP 2, 7]
9: (A → (B → ⊥)) → (A → (B → C)) [MP 1, 8]

La prueba final:
1: (((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) → ((((A → (B → ⊥)) → ⊥) → (( A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A)) [cadena]
2: (((A → ⊥) → A) → A) → (((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) [Verum Ex] < br> 3: ((A → ⊥) → A) → A [Mirabilis]
4: ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A) [MP 2, 3] | 5: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A) [MP 1, 4 ]
6: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) [Lemma 2]
7: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) [Lemma 1] | 8: ((A → ⊥) → (A → (B → ⊥))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥) ))) [Verum Ex]
9: ((A → ⊥) → (A → ⊥)) → ((A → ⊥) → (A → (B → ⊥))) [Lemma 2]
10: ((A → ⊥) → (A → A)) → ((A → ⊥) → (A → ⊥)) [Lemma 1] | 11: (A → A) → ((A → ⊥) → (A → A)) [Verum Ex]
12: A → A [Identidad]
13: (A → ⊥) → (A → A) [MP 11, 12]
14: (A → ⊥) → (A → ⊥) [MP 10, 13]
15: (A → ⊥) → (A → (B → ⊥)) [MP 9, 14]
16: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥))) [MP 8, 15]
17: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥) [MP 7, 16]
18: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A) [MP 6, 17]
19: ((A → (B → ⊥)) → ⊥) → A [MP 5, 18]

Toda una larga prueba!

adiós

  1. ¿Qué sistema específico de Hilbert? Hay toneladas.
  2. Probablemente la mejor manera es encontrar una prueba en un cálculo secuencial y convertirlo en el sistema de Hilbert.

notación polaca .

Desde que hizo referencia la Wikipedia, vamos a suponer nuestra base es

1 CpCqp.

2 CCpCqrCCpqCpr.

3 CCNpNqCqp.

Queremos demostrar

NCaNb | -. A

Yo uso el teorema de prover Prover9 . Por lo tanto, tendremos que poner entre paréntesis todo. Además, las variables de Prover9 van (x, y, z, u, w, V5, V6, ..., vn). Todos los otros símbolos va a interpretar como funciones o relaciones o predicados. Todos los axiomas necesitan un símbolo de predicado "P" delante de ellos también, que podemos pensar en el sentido de "que es demostrable que ...", o más simplemente "demostrable". Y todas las sentencias en Prover9 necesitan conseguir terminado por un punto. Por lo tanto, axiomas 1, 2, y 3 se convierten respectivamente:

1 P (C (x, C (y, x))).

2 P (C (C (x, C (y, z)), C (C (x, y), C (x, z)))).

3 P (C (C (N (x), N (y)), C (y, x))).

Podemos combinar las reglas de sustitución uniforme y desprendimiento en el estado de condensada desprendimiento . En Prover9 podemos representar esto como:

-P (C (x, y)) | -P (x) | P (y).

El "|" disyunción lógica indica, y "-" indica negación. Prover9 prueba por contradicción. La regla dice en las palabras pueden quedar interpretado como diciendo "ya sea que no es el caso de que si X, entonces Y es demostrable, o que no es el caso que x es demostrable, o Y es demostrable". Por lo tanto, si lo hace espera que si x, entonces y es demostrable, la primera disyunción falla. Si lo hace espera que x es demostrable, entonces la segunda disyunción falla. Por lo tanto, si, si x, entonces y es demostrable, si x es demostrable, entonces el tercer disjunta, que y es demostrable por la siguiente regla.

Ahora no podemos hacer sustituciones en NCaNb, ya que no es una tautología. Tampoco es "a". Por lo tanto, si ponemos

P (N (C (a, N (b)))).

como un supuesto, Prover9 interpretará "a" y "b" como nullary funciones, que los convierte efectivamente en constantes. También queremos hacer P (a) como nuestro objetivo.

Ahora también podemos "afinar" Prover9 utilizando diversas estrategias de tipo teorema que demuestra como la ponderación, la resonancia, la subfórmula, relación dada-Pick, la saturación del nivel (o incluso inventar nuestro propio). Voy a usar la estrategia consejos un poco, por lo que todos los supuestos (incluyendo la regla de inferencia), y la meta en consejos. También voy a su vez el peso máximo de hasta 40, y hago 5 el número máximo de variables.

Yo uso la versión con la interfaz gráfica, pero aquí está la entrada completa: 

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, -1).
assign(max_weight, 40).
end_if.

if(Mace4).   % Options for Mace4
assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
formulas(hints).
-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).
P(a).
end_of_list.
assign(max_vars,5).
end_if.

formulas(assumptions).

-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).

end_of_list.

formulas(goals).

P(a).

end_of_list.

Aquí está la prueba que me dio: 

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 1312 was started by Doug on Machina2,
Mon Jun  9 22:35:37 2014
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace43/bin-win32/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 23.
% Level of proof is 9.
% Maximum clause weight is 20.
% Given clauses 49.

1 P(a) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 P(N(C(a,N(b)))).  [assumption].
7 -P(a).  [deny(1)].
8 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
9 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
12 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
13 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,N(C(a,N(b))))).  [hyper(2,a,3,a,b,6,a)].
23 P(C(C(a,N(b)),x)).  [hyper(2,a,5,a,b,14,a)].
28 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,9,a,b,8,a)].
30 P(C(x,C(C(a,N(b)),y))).  [hyper(2,a,3,a,b,23,a)].
33 P(C(C(x,C(a,N(b))),C(x,y))).  [hyper(2,a,4,a,b,30,a)].
103 P(C(N(b),x)).  [hyper(2,a,33,a,b,3,a)].
107 P(C(x,b)).  [hyper(2,a,5,a,b,103,a)].
113 P(C(C(N(x),N(b)),x)).  [hyper(2,a,12,a,b,107,a)].
205 P(C(N(x),C(x,y))).  [hyper(2,a,28,a,b,13,a)].
209 P(C(N(a),x)).  [hyper(2,a,33,a,b,205,a)].
213 P(a).  [hyper(2,a,113,a,b,209,a)].
214 $F.  [resolve(213,a,7,a)].

============================== end of proof ==========================
Licenciado bajo: CC-BY-SA con atribución
No afiliado a StackOverflow
scroll top