Espoleado por Willemien de la competencia, pensé que había puesto mi propia.
En 1948, un papel por Jan Lukasiewicz se publicó que estableció un 13 de la carta de la fórmula (uno de?) el menor solo axiomas, en virtud del desprendimiento, de la pura implicational cálculo de proposiciones (Lukasiewicz había reclamado lo siguiente como un único axioma tan atrás como el año 1937, pero no hay pruebas de que había publicado hasta 1948).
L. CCCpqrCCrpCsp (((p→q)→r)→((r→p)→(s→p)))
La formulación original de implicational cálculo proposicional por Tarski y Bernays había tres axiomas junto con el desprendimiento.
1. CCpqCCqrCpr ((p→q)→((q→r)→(p→r)))
2. CpCqp (p→(q→p))
3. CCCpqpp (((p→q)→p)→p)
Supongamos que partimos de 1., 2., 3. y quiere deducir L. y tiene dos reglas de inferencia 1. condensada desprendimiento, y 2, condensada silogismo, de la siguiente manera:
Condensada desprendimiento nos permite inferir, a partir de C$\alpha$$\beta$ y $\alpha$' a $\beta$", donde $\alpha$' e $\alpha$ tiene un unificador más general, y que ninguna de las variables no se ven afectados por la unificación de las $\alpha$' e $\alpha$ el cambio de variables distintos de los de otras variables. Por un unificador, quiero decir que existe una forma común de obtener de $\alpha$ y también de $\alpha$' solo haciendo sustituciones en $\alpha$$\alpha$', la cual es única hasta volver a las letras de las variables. Nos deja denotar una aplicación de condensados desprendimiento con x como C$\alpha$$\beta$, e y como $\alpha$ "por" Dx.y".
Condensada silogismo, del mismo modo, nos permite inferir, a partir de C$\alpha$$\beta$ y C$\beta$'$\gamma$ a C$\alpha$"$\gamma$", donde $\beta$ $\beta$ ' tienen más general unificador y que ninguna de las variables no se ven afectados por la unificación de las $\beta$' e $\beta$ el cambio de variables distintos de los de otras variables. De nuevo, quiero decir que existe una forma común de obtener de $\beta$ $\beta$ ' por la sustitución solo (sustituciones pueden obtener tanto $\beta$ y en $\beta$') que es único para re-letras de variables. Nos deja denotar una aplicación de condensados silogismo con x como C$\alpha$$\beta$, e y como C$\beta$'$\gamma$ por "Sx.y".
Para condensados desprendimiento podemos sacar algo como esto,
1 C C p q CCqrCpr
| | |
| | ---
2 C p Cqp
Por Lo Tanto, D1.2 rendimientos de 4 CCCqprCpr.
4 C CC q p r Cpr
|| | | |
|| --- | |
3 CC Cpq p p
Así, D4.3 rendimientos de 5 Cpp.
Para condensados silogismo podemos sacar algo como esto:
2 Cp C q p
| | |
| --- |
3 C C Cpq p p
Así, S2.3 rendimientos de Cpp.
El uso de las reglas de condensados silogismo y condensada desprendimiento, lo que es el más corto de la prueba en términos de número de pasos de CCCpqrCCrpCsp?
Por favor, anote sus pruebas de la siguiente manera (aunque la notación de infijo):
1 CCpqCCqrCpr
2 CpCqp
3 CCCpqpp
S3.2 4 CCCpqpCqp
S4.1 5 CCCqpqCCprCqr
D1.4 6 CCCqprCCCpqpr.
Las reglas de la competencia:
Voy a darle a la persona que viene con la menor prueba de una recompensa de 200 (sin marcar) puntos de reputación. Sólo puedo añadir una recompensa en un par de días a partir de ahora, pero puedes publicar tu respuesta ahora.
La longitud de una prueba se mide por el número de líneas numeradas de la prueba (véase la prueba anterior como un ejemplo, la primera fórmula es en el número de línea 1, y cada prueba de línea se cuentan por igual, no importa si usted utiliza condensada desprendimiento o condensada silogismo)
La regla de desempate : Si hay más de una persona con la respuesta más corta que la recompensa va el cartel con la mayoría de los casos de condensados desprendimiento de usa. Si eso no resuelve los empates, a continuación, la recompensa se ve el cartel que ha publicado la prueba con el menor símbolo count (excluyendo paréntesis) de las más largas de la fórmula en la prueba.
La respuesta debe tener la forma de una completa axiomática de la deducción como la prueba de CCCqprCCCpqpr arriba.
Usted puede dar más de una respuesta, respuestas en más de una prueba método etc, pero post como separada de respuestas, y ser conscientes de que sólo la prueba de que utiliza el sistema axiomático con las reglas de condensados de desprendimiento y/o condensada silogismo anterior es competir, y a los otros participantes pueden ver sus respuestas.
Por favor no borrar sus respuestas.
Re-letras de variables que van a ser ignorada, por lo cual quiero decir que si después de una prueba de CCCabcCCcaCda que va a ser contado como una prueba de la misma manera que una prueba de CCCpqrCCrpCsp va a ser contado, y similares.
Usted puede utilizar un teorema de armario, pero por favor escriba su respuesta en notación polaca o estándar infix notation (notación polaca inversa con "C" como el conectivo voy a aceptar también).
Mejor de los éxitos, y que gane el mejor.
