math - pruebas - testing automatizado

Sistema Hilbert-Automatizar Pruebas

Question

Estoy tratando de probar la declaración ~ (a-> ~ b) => a en un sistema de estilo Hilbert . Desafortunadamente, parece que es imposible encontrar un algoritmo general para encontrar una prueba, pero estoy buscando una estrategia de tipo fuerza bruta. Cualquier idea sobre cómo atacar esto es bienvenida.

Answer 1

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

Answer 2

El sistema de Hilbert no se usa normalmente en la prueba automatizada de teoremas. Es mucho más fácil escribir un programa de computadora para hacer pruebas usando deducción natural. Del material de un curso de CS :

Algunas preguntas frecuentes sobre el sistema de Hilbert: P: ¿Cómo se sabe qué esquemas de axiomas usar y qué sustituciones se deben hacer? Ya que hay infinitas posibilidades, no es posible probarlas todas, incluso en principio. A: No hay algoritmo; Al menos ninguna simple. Más bien, uno tiene que ser inteligente. En matemáticas puras, esto no se ve como un problema, ya que uno está más preocupado por la existencia de una prueba. Sin embargo, en aplicaciones informáticas, uno está interesado en automatizar el proceso de deducción, por lo que este es un defecto fatal. El sistema de Hilbert no se usa normalmente en la prueba automatizada de teoremas. P: Entonces, ¿por qué a la gente le importa el sistema de Hilbert? R: Con modus ponens como su única regla deductiva, proporciona un modelo aceptable de cómo los humanos diseñan pruebas matemáticas. Como veremos, los métodos que son más susceptibles a la implementación en computadora producen pruebas que son menos "similares a las de los humanos".

Answer 3

Encontrar pruebas en el cálculo de Hilbert es muy difícil.

Podrías intentar traducir pruebas en cálculo secuencial o deducción natural al cálculo de Hilbert.

Answer 4

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

• Puede "traducir" automáticamente algunos problemas de lógica a otro campo: probar la igualdad de los términos de lógica combinatoria.
• Con una buena práctica de programación funcional, puedes resolver eso,
• y luego, puede volver a traducir la respuesta a una prueba del estilo de Hilbert de su problema lógico original.

La posibilidad de esta traducción está garantizada por la correspondencia Curry-Howard .

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

¬ ( α ⊃ ¬ β ) ⊢ α

Pero en los casos en que la negación no es parte de la pregunta, la traducción automática mencionada (y la traducción inversa) pueden ser una ayuda, siempre que ya haya practicado en programación funcional o lógica combinatoria.

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

• Probar el problema en algún sistema deductivo más intuitivo (por ejemplo, deducción natural )
• y luego usar metatheorem s que brindan una posibilidad de "compilación": traducir la prueba de deducción natural de "alto nivel" al "código de máquina" del sistema de deducción de estilo Hilbert. Me refiero, por ejemplo, al teorema metalógico llamado " teorema de deducción ".

En cuanto a los probadores de teoremas, que yo sepa, las capacidades de algunos de ellos se amplían para que puedan aprovechar la asistencia humana interactiva. Por ejemplo, Coq es tal.

Apéndice

Veamos un ejemplo. ¿Cómo probar α ⊃ α ?

Sistema de hilbert

• Verum ex quolibet _{α , β} se asume como un esquema axiomático, indicando que se espera que la oración α ⊃ β expected α sea ​​deducible, instanciada para cualquier subsentencia α , β
• La regla de la cadena _{α , β , γ} se asume como un esquema axiomático, que indica que la oración ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ se espera que sea deducible, instanciada para cualquier subsentencia α , β
• El modus ponens se asume como una regla de inferencia: siempre que α ⊃ β sea ​​deducible, y también α sea ​​deducible, entonces esperamos estar justificados para inferir que también α ⊃ β es deducible.

Probemos el teorema: α ⊃ α es deducible para cualquier proposición α .

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

Cálculo de prueba

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

Una notación de diagrama de árbol:

Esquema de axiomas - Verum ex quolibet:

━━━━━━━━━━━━━━━━━ [ VEQ _{α , β} ]
⊢ α ⊃ β ⊃ α

Esquema de axiomas - regla de la cadena:

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

Regla de inferencia - modus ponens:

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

Arbol de prueba

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

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

Fórmulas de prueba

Veamos una representación concisa (algebraica? Cálculo?) De la prueba:

( CR _{α , α ⊃ α , α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢ α ⊃ α

Por lo tanto, podemos representar el árbol de prueba mediante una única fórmula:

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

Vale la pena mantener un registro de la creación de instancias concreta, que se compone aquí con parámetros subindexicos.

Como se verá en la siguiente serie de ejemplos, podemos desarrollar un cálculo de prueba , donde los axiomas se mencionan como una especie de combinadores de base , y el modus ponens se menciona como una mera aplicación de sus sub-pruebas "premisas":

Ejemplo 1

VEQ _{α , β} : ⊢ α ⊃ β ⊃ α

significado como

El esquema de Verum ex quolibet axiom instanciado con α , β proporciona una prueba de la afirmación de que α ⊃ β ⊃ α es deducible.

Ejemplo 2

VEQ _{α , α} : ⊢ α ⊃ α ⊃ α

El esquema de Verum ex quolibet axiom instanciado con α , α proporciona una prueba de la afirmación de que α ⊃ α ⊃ α es deducible.

Ejemplo 3

VEQ _{α , α ⊃ α} : ⊢ α ⊃ ( α ⊃ α ) ⊃ α

significado como

El esquema de Verum ex quolibet axiom instanciado con α , α ⊃ α proporciona una prueba de la afirmación de que α ⊃ ( α ⊃ α ) ⊃ α es deducible.

Ejemplo 4

CR _{α , β , γ} : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

significado como

El esquema del axioma de la regla de la cadena instanciado con α , β , γ proporciona una prueba de la afirmación de que ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ es deducible.

Ejemplo 5

CR _{α , α ⊃ α , α} : ⊢ [ α ⊃ ( α ⊃ α ) ⊃ α ] ⊃ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α

significado como

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

Ejemplo 6

CR _{α , α ⊃ α , α} VEQ _{α , α ⊃ α} : ⊢ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α

significado como

Si combinamos CR _{α , α ⊃ α , α} y VEQ _{α , α ⊃ α} juntos a través de modus ponens , entonces obtenemos una prueba que prueba la siguiente afirmación: ( α ⊃ α ⊃ α ) ⊃ α ⊃ α es deducible.

Ejemplo 7

( CR _{α , α ⊃ α , α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢ α ⊃ α

Si combinamos la prueba de compuesto ( CR _{α , α ⊃ α , α} ) junto con VEQ _{α , α ⊃ α} (a través de modus ponens ), obtenemos una prueba aún más compund. Esto prueba la siguiente afirmación: α ⊃ α es deducible.

Lógica combinatoria

Aunque todo lo anterior ha proporcionado una prueba para el teorema esperado, pero parece muy poco intuitivo. No se puede ver cómo las personas pueden "descubrir" la prueba.

Veamos otro campo, donde se investigan problemas similares.

Lógica combinatoria sin tipo

La lógica combinatoria puede considerarse también como un lenguaje de programación funcional extremadamente minimalista. A pesar de su minimalismo, Turing está completamente completo, pero aún más, uno puede escribir programas bastante intuitivos y complejos incluso en este lenguaje aparentemente confuso, de manera modular y reutilizable, con algo de práctica obtenida de la programación funcional "normal" y algunas ideas algebraicas. .

Agregando reglas de escritura

La lógica combinatoria también tiene variantes tipificadas. La sintaxis está aumentada con tipos, y aún más, además de las reglas de reducción, también se agregan reglas de escritura.

Para combinadores de base:

• K _{α , β} se selecciona como un combinador básico, que habita el tipo α → β → α
• S _{α , β , γ} se selecciona como un combinador básico, que habita el tipo ( α → β → γ ) → ( α → β ) → α → γ .

Escribiendo regla de aplicación:

• Si X habita el tipo α → β e Y habita el tipo α , entonces X Y habita el tipo β .

Notaciones y abreviaturas.

• K _{α , β} : α → β → α
• S _{α , β , γ} : ( α → β → γ ) → ( α → β ) * → α → γ .
• Si X : α → β e Y : α , entonces X Y : β .

Correspondencia Curry-Howard

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

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

Programacion funcional

Pero ¿cuál es la ganancia? ¿Por qué deberíamos traducir los problemas a la lógica combinatoria? Yo, personalmente, lo encuentro a veces útil, porque la programación funcional es una cosa que tiene una gran cantidad de literatura y se aplica en problemas prácticos. La gente puede acostumbrarse a ella, cuando se la obliga a usarla en las tareas de programación de cada día y en la práctica. Y algunos trucos y sugerencias de la práctica de la programación funcional pueden explotarse muy bien en reducciones de lógica combinatoria. Y si una práctica "transferida" se desarrolla en lógica combinatoria, también puede aprovecharse para encontrar pruebas en el sistema de Hilbert.

enlaces externos

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

• Wadler, Philip (1989). Teoremas de forma gratuita! .

Enlaces (o libros) sobre cómo aprender métodos y practicar para programar directamente en lógica combinatoria:

• Madore, David (2003). El lenguaje de programación Unlambda. Unlambda: tus pesadillas en el lenguaje de programación funcional se hacen realidad .
• Curry, Haskell B. y Feys, Robert y Craig, William (1958). Lógica combinatoria . Vol. Yo Amsterdam: Compañía de Publicaciones de Holanda Septentrional.
• Tromp, John (1999). Cálculo Lambda Binario y Lógica Combinatoria . Descargable en PDF y PostScript de John''s Lambda Calculus y Combinatory Logic Playground .

Answer 5

También puede abordar el problema configurando ¬ α = α → ⊥. Luego podemos adoptar el sistema de estilo de Hilbert como se muestra en el apéndice de una de las respuestas, y hacerlo clásico agregando las siguientes dos constantes de axiomas y respectivamente:

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

Una prueba secuencial de ¬ (α → ¬ β) → α se lee de la siguiente manera:

1. α ⊢ α (identidad)
2. ⊥ ⊢ β → ⊥ (Ex Falso Quodlibet)
3. α → ⊥, α ⊢ β → ⊥ (Impl Intro Left 1 & 2)
4. α → ⊥ ⊢ α → (β → ⊥) (Impl Intro Right 3)
5. ⊥ ⊢ α (Ex Falso Quodlibet)
6. (α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (Impl Intro Left 4 & 5)
7. (α → (β → ⊥)) → ⊥ ⊢ α (Consequentia Mirabilis 6)
8. ⊢ ((α → (β → ⊥)) → ⊥) → α (Impl Intro Right 7)

A partir de esta prueba secuencial, uno puede extraer una expresión lambda. Una posible expresión lambda para la prueba secuencial anterior dice lo siguiente:

λy. (M λz. (E (y λx. (E (zx)))))

Esta expresión lambda se puede convertir en un término SKI. Un posible término de SKI para la expresión lambda anterior dice lo siguiente:

S (KM)) (L2 (L1 (K (L2 (L1 (KI))))))
donde L1 = (S ((S (KS)) ((S (KK)) I))))
y L2 = (S (K (S (KE))))

Esto da las siguientes pruebas de estilo de Hilbert:

Lemma 1: Una forma debilitada de la regla de la cadena:
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]
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 debilitada de Ex Falso:
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]

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]
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 → ⊥))) [Lema 2]
10: ((A → ⊥) → (A → A)) → ((A → ⊥) → (A → ⊥)) [Lema 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]

¡Una prueba bastante larga!

Adiós

Answer 6

Yo uso la notación polaca .

Desde que hiciste referencia a la Wikipedia, supondremos que nuestra base es

1 CpCqp.

2 CCpCqrCCpqCpr.

3 CCNpNqCqp.

Queremos probar

NCaNb | - a.

Yo uso el Prover9 teorema. Entonces, necesitaremos paréntesis de todo. Además, las variables de Prover9 van (x, y, z, u, w, v5, v6, ..., vn). Todos los demás símbolos se interpretan como funciones o relaciones o predicados. Todos los axiomas también necesitan un símbolo de predicado "P" delante de ellos, que podemos pensar que significa "es demostrable que ..." o más simplemente "demostrable". Y todas las oraciones en Prover9 deben terminar por un punto. Así, los 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 la regla de detachment condensed . En Prover9 podemos representar esto como:

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

El "|" indica disyunción lógica, y "-" indica negación. Prover9 prueba por contradicción. La regla dice que con palabras se puede interpretar diciendo que "o no es el caso de que si x, entonces y es demostrable, o no es el caso de que x es demostrable, o y es demostrable". Por lo tanto, si mantiene que si x, entonces y es demostrable, el primer disyuntar falla. Si mantiene que x es demostrable, entonces el segundo disyuntar falla. Entonces, si, si x, entonces y es demostrable, si x es demostrable, entonces el tercer disyuntivo, esa y es demostrable sigue la regla.

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

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

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

Ahora también podemos "sintonizar" Prover9 utilizando diversas estrategias de demostración de teoremas, como ponderación, resonancia, subformula, relación de selección, saturación de nivel (o incluso inventar la nuestra). Usaré la estrategia de sugerencias un poco, al hacer todas las suposiciones (incluida la regla de inferencia) y el objetivo en sugerencias. También reduciré el peso máximo a 40 y haré que 5 sea el número de variables máximas.

Utilizo 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 ==========================