11 casos · validados manualmenteautologic · reglas, sin LLM

Casos validados — NLP a lógica formal

Estos son argumentos reales (jurídicos, filosóficos, matemáticos) formalizados automáticamente por autologic y comparados con la respuesta manual esperada. Todos los casos están en la suite de tests de auto.logic (docs/validated-hard-cases-comparison.md). Puedes cargar cualquiera en el playground y ejecutarlo en vivo.

Abrir playground →Documentación ST →

classical.propositionalmodus_ponens

Modus ponens clásico

El patrón de inferencia más básico: de A→B y A se deriva B. Verificación de tautología incluida.

Abrir en playground →

Texto natural (entrada)

Si llueve, entonces la calle se moja. Está lloviendo. Por lo tanto, la calle se moja.

Codigo ST generado (extracto)

logic classical.propositional

axiom regla_1 : LLUEVE -> CALLE_MOJA
axiom hecho_2 : LLOVIENDO

derive CALLE_MOJA from {regla_1, hecho_2}
check valid (LLUEVE -> CALLE_MOJA)

Nota tecnica: El formalizador detecta "si... entonces" como condicional, "está lloviendo" como hecho y "por lo tanto" como marcador de conclusión. Emite derive + check valid.

classical.propositionalmodus_tollens

Modus tollens

Negación del consecuente implica negación del antecedente: ¬B, A→B ⊢ ¬A.

Abrir en playground →

Texto natural (entrada)

Si llueve, entonces la calle se moja. La calle no se moja. Por lo tanto, no llueve.

Codigo ST generado (extracto)

logic classical.propositional

axiom regla_1 : LLUEVE -> CALLE_MOJA
axiom neg_2   : !(CALLE_MOJA)

derive !(LLUEVE) from {regla_1, neg_2}
check valid ((LLUEVE -> CALLE_MOJA) & !(CALLE_MOJA) -> !(LLUEVE))

Nota tecnica: "no se moja" activa el extractor de negación. El formalizador emite axiom neg_N con negación explícita.

classical.propositionalhypothetical_syllogismconditional_chain

Silogismo hipotético

Cadena condicional: A→B, B→C ⊢ A→C. El formalizador detecta el patrón hypothetical_syllogism.

Abrir en playground →

Texto natural (entrada)

Si estudio, entonces aprendo. Si aprendo, entonces apruebo el examen. Por lo tanto, si estudio, apruebo el examen.

Codigo ST generado (extracto)

logic classical.propositional

axiom regla_1 : ESTUDIO -> APRENDO
axiom regla_2 : APRENDO -> APRUEBO_EXAMEN

derive ESTUDIO -> APRUEBO_EXAMEN from {regla_1, regla_2}
check valid ((ESTUDIO -> APRENDO) & (APRENDO -> APRUEBO_EXAMEN) -> (ESTUDIO -> APRUEBO_EXAMEN))

Nota tecnica: El patrón hypothetical_syllogism encadena dos condicionales. El check valid confirma que la transitividad es una tautología proposicional.

classical.propositionalmodus_ponenshypothetical_syllogismconditional_chainconjunction_introduction

Obligacion contractual — despachar equipo

Cadena condicional de 3 eslabones con conjunción. Caso jurídico real de derecho contractual.

Abrir en playground →

Texto natural (entrada)

Si el contrato fue firmado por el apoderado con poder vigente, entonces el acuerdo es formalmente válido. Si el acuerdo es formalmente válido y el pago inicial fue consignado, entonces se activa la obligación de entrega. Si se activa la obligación de entrega, entonces la empresa debe despachar el equipo. El apoderado tenía poder vigente y firmó el contrato. El pago inicial fue consignado. Por lo tanto, la empresa debe despachar el equipo.

Codigo ST generado (extracto)

logic classical.propositional

axiom regla_1 : APODERADO_VIGENTE -> ACUERDO_VALIDO
axiom regla_3 : ACUERDO_VALIDO -> OBLIGACION_ENTREGA
axiom regla_5 : OBLIGACION_ENTREGA -> DESPACHAR_EQUIPO
axiom hecho_9 : APODERADO_VIGENTE
axiom hecho_10 : PAGO_CONSIGNADO

derive DESPACHAR_EQUIPO from {regla_1, regla_3, regla_5, hecho_9, hecho_10}

Nota tecnica: Uno de los 11 casos hard validados de auto.logic. El formalizador encadena 3 condicionales con modus ponens repetido y detecta la conjunción de hechos.

deontic.standardmodus_ponensuniversal_generalizationuniversal_instantiation

Plagio academico — obligacion y prohibicion

Caso de lógica deóntica: detección de plagio activa obligación de suspensión y prohibición de publicación.

Abrir en playground →

Texto natural (entrada)

Todo revisor académico que detecte plagio grave está obligado a suspender la evaluación y a reportar el caso al comité de ética. Ningún coordinador editorial puede autorizar la publicación de un manuscrito suspendido. En este caso, el revisor detectó plagio grave. Por lo tanto, es obligatorio suspender la evaluación y está prohibido autorizar la publicación del manuscrito.

Codigo ST generado (extracto)

logic deontic.standard

axiom a1 = EVALUACION_ACADEMICO_SUSPENDER_OBLIGADO
axiom a2 = REPORTAR_COMITE_ETICA_CASO
axiom a3 = !(COORDINADOR_PUBLICACION_MANUSCRITO_SUSPENDIDO)
axiom a8 = O(OBLIGATORIO_EVALUACION_SUSPENDER)
axiom a10 = PUBLICACION_MANUSCRITO_PROHIBIDO_AUTORIZAR

check valid (AUTORIZACION_EXCEPCIONAL -> P(PERMITIDO_REANUDAR_REVISION))

Nota tecnica: Caso hard validado. El perfil deontic.standard genera operadores O() (obligación) y P() (permisión). "ningún" activa negación sobre el cuantificador universal.

aristotelian.syllogisticuniversal_generalizationuniversal_instantiationconjunction_introduction

Peritos acreditados y dictámenes — silogística

Razonamiento jurídico aristotélico: universal + negación + instanciación múltiple sobre suspensión de peritos.

Abrir en playground →

Texto natural (entrada)

Todo perito acreditado que actúa en causas penales es auxiliar de la justicia. Ningún auxiliar de la justicia con suspensión vigente puede emitir dictamen vinculante. Todo dictamen vinculante integra el expediente principal. Por lo tanto, ningún perito acreditado con suspensión vigente puede emitir dictamen vinculante.

Codigo ST generado (extracto)

logic aristotelian.syllogistic

axiom a1 = forall x auxili(x)
axiom a2 = SUSPENSION_VINCULANTE_AUXILIAR_JUSTICIA
axiom a3 = forall x dictam(x)

derive ACREDITADO_PENALES_NINGUN_PERITO from {a1, a2, a3, ...}
check valid ((...) -> ACREDITADO_PENALES_NINGUN_PERITO)

Nota tecnica: Caso hard validado. El formalizador identifica "todo" → forall, "ningún" → negación universal, y construye la regla de instanciación universal sobre los átomos extraídos.

epistemic.s5modus_ponenshypothetical_syllogism

Llave maestra — conocimiento anidado

Epistémica S5: conocimiento del administrador sobre acceso, con introspección positiva K(P)→K(K(P)).

Abrir en playground →

Texto natural (entrada)

El administrador sabe que la llave maestra abre todas las puertas del edificio. Si el administrador sabe que la llave maestra abre todas las puertas, entonces el administrador sabe que puede acceder a cualquier sala. Por lo tanto, el administrador puede acceder a cualquier sala.

Codigo ST generado (extracto)

logic epistemic.s5

axiom a1 = K_admin(LLAVE_ABRE_PUERTAS)
axiom a2 = K_admin(LLAVE_ABRE_PUERTAS) -> K_admin(PUEDE_ACCEDER_SALA)

derive K_admin(PUEDE_ACCEDER_SALA) from {a1, a2}

Nota tecnica: Caso hard validado. El operador K_agente() se genera cuando el formalizador detecta "sabe que" seguido de un nombre de agente en el contexto epistémico S5.

classical.propositionalhypothetical_syllogismmodus_ponens

Argumento kantiano — intuición pura y geometría

Formalización de la Crítica de la Razón Pura: cadena hipotética sobre intuición pura → geometría euclidiana posible.

Abrir en playground →

Texto natural (entrada)

Si hay intuición pura, entonces es posible el juicio sintético a priori. Si es posible el juicio sintético a priori, entonces la geometría euclidiana es posible. Hay intuición pura del espacio y del tiempo. Por lo tanto, la geometría euclidiana es posible.

Codigo ST generado (extracto)

logic classical.propositional

axiom kant1 : INTUICION_PURA -> JUICIO_SINTETICO
axiom kant2 : JUICIO_SINTETICO -> GEOMETRIA_POSIBLE
axiom kant3 : INTUICION_PURA

derive GEOMETRIA_POSIBLE from {kant1, kant2, kant3}
check valid (((INTUICION_PURA -> JUICIO_SINTETICO) & (JUICIO_SINTETICO -> GEOMETRIA_POSIBLE) & INTUICION_PURA) -> GEOMETRIA_POSIBLE)

Nota tecnica: Ejemplo filosófico de la Text Layer de ST. La cadena hipotética es una tautología proposicional: ((A→B)&(B→C)&A)→C. El check valid lo confirma.

temporal.ltlmodus_ponens

Falla y alerta — LTL

Lógica temporal lineal: propiedad de safety/liveness sobre sistemas de monitoreo de fallas.

Abrir en playground →

Texto natural (entrada)

Siempre que se detecte una falla, eventualmente se debe emitir una alerta. Se detectó una falla. Por lo tanto, eventualmente se emitirá una alerta.

Codigo ST generado (extracto)

logic temporal.ltl

axiom regla : G(FALLA_DETECTADA -> F(ALERTA_EMITIDA))
axiom hecho : FALLA_DETECTADA

prove F(ALERTA_EMITIDA)

Nota tecnica: Operadores LTL: G (globally / siempre), F (finally / eventualmente). El formalizador detecta "siempre que" → G(…→…) y "eventualmente" → F(…).

modal.kmodus_ponens

Necesidad de las leyes — Modal K

Lógica modal básica (sistema K): necesidad de las leyes implica posibilidad de sanción.

Abrir en playground →

Texto natural (entrada)

Es necesario que las leyes se cumplan. Si es necesario que las leyes se cumplan, entonces es posible sancionar.

Codigo ST generado (extracto)

logic modal.k

axiom a1 : □(LEYES_CUMPLAN)
axiom a2 : □(LEYES_CUMPLAN) -> ◇(SANCIONAR)

prove ◇(SANCIONAR)

Nota tecnica: "Es necesario que" → □(P) (operador de necesidad). "es posible" → ◇(P) (operador de posibilidad). Sistema K: sin axiomas adicionales de accesibilidad.

aristotelian.syllogisticuniversal_instantiation

Silogismo Barbara — todo humano es mortal

El silogismo clásico más conocido: ∀x(H(x)→M(x)), H(s) ⊢ M(s). Aristotelian.syllogistic.

Abrir en playground →

Texto natural (entrada)

Todo ser humano es mortal. Sócrates es un ser humano. Por lo tanto, Sócrates es mortal.

Codigo ST generado (extracto)

logic aristotelian.syllogistic

axiom mayor : forall x (humano(x) -> mortal(x))
axiom menor : humano(socrates)

derive mortal(socrates) from {mayor, menor}

Nota tecnica: Forma Barbara (AAA-1). "Todo" → forall, "es" (cópula) → predicado. El perfil aristotelian.syllogistic reconoce las cuatro formas categóricas: A (todo), E (ningún), I (algún), O (algún... no).

Cómo se generan estas formalizaciones

1. Segmentación

El texto se divide en oraciones y cláusulas usando stemmers Snowball y análisis de puntuación. Cada cláusula se clasifica según su función discursiva (premisa, conclusión, negación, condicional...).

2. Detección de patrones

~200 marcadores discursivos en ES/EN ("si... entonces", "por lo tanto", "todo", "ningún", "es obligatorio"...) activan patrones de inferencia: modus_ponens, hypothetical_syllogism, universal_generalization, etc.

3. Emisión ST

Los átomos extraídos se nombran con keywords del texto. Las reglas de inferencia detectadas se traducen a axiomas, derives y checks del perfil lógico seleccionado. El resultado es código ST ejecutable que produce derivaciones verificables.