11 casos · validados manualmenteautologic · reglas, sin LLM

Casos validados — NLP a logica formal

Estos son argumentos reales (juridicos, filosoficos, matematicos) formalizados automaticamente por autologic y comparados con la respuesta manual esperada. Todos los casos estan 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 →Documentacion ST →
classical.propositionalmodus_ponens

Modus ponens clasico

El patron de inferencia mas basico: de A→B y A se derive B. Verificacion de tautologia 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 conclusion. Emite derive + check valid.

classical.propositionalmodus_tollens

Modus tollens

Negacion del consecuente implica negacion 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 negacion. El formalizador emite axiom neg_N con negacion explicita.

classical.propositionalhypothetical_syllogismconditional_chain

Silogismo hipotetico

Cadena condicional: A→B, B→C ⊢ A→C. El formalizador detecta el patron 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 patron hypothetical_syllogism encadena dos condicionales. El check valid confirma que la transitividad es una tautologia proposicional.

classical.propositionalmodus_ponenshypothetical_syllogismconditional_chainconjunction_introduction

Obligacion contractual — despachar equipo

Cadena condicional de 3 eslabones con conjuncion. Caso juridico 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 conjuncion de hechos.

deontic.standardmodus_ponensuniversal_generalizationuniversal_instantiation

Plagio academico — obligacion y prohibicion

Caso de logica deontica: deteccion de plagio activa obligacion de suspension y prohibicion de publicacion.

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() (obligacion) y P() (permision). "ningun" activa negacion sobre el cuantificador universal.

aristotelian.syllogisticuniversal_generalizationuniversal_instantiationconjunction_introduction

Peritos acreditados y dictamenes — silogistica

Razonamiento juridico aristotelico: universal + negacion + instanciacion multiple sobre suspension 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, "ningun" → negacion universal, y construye la regla de instanciacion universal sobre los atomos extraidos.

epistemic.s5modus_ponenshypothetical_syllogism

Llave maestra — conocimiento anidado

Epistemica 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 epistemico S5.

classical.propositionalhypothetical_syllogismmodus_ponens

Argumento kantiano — intuicion pura y geometria

Formalizacion de la Critica de la Razon Pura: cadena hipotetica sobre intuicion pura → geometria 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 filosofico de la Text Layer de ST. La cadena hipotetica es una tautologia proposicional: ((A→B)&(B→C)&A)→C. El check valid lo confirma.

temporal.ltlmodus_ponens

Falla y alerta — LTL

Logica 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

Logica modal basica (sistema K): necesidad de las leyes implica posibilidad de sancion.

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 clasico mas 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" (copula) → predicado. El perfil aristotelian.syllogistic reconoce las cuatro formas categoricas: A (todo), E (ningun), I (algun), O (algun... no).

Como se generan estos formalizaciones

1. Segmentacion

El texto se divide en oraciones y clausulas usando stemmers Snowball y analisis de puntuacion. Cada clausula se clasifica segun su funcion discursiva (premisa, conclusion, negacion, condicional...).

2. Deteccion de patrones

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

3. Emision ST

Los atomos extraidos se nombran con keywords del texto. Las reglas de inferencia detectadas se traducen a axiomas, derives y checks del perfil logico seleccionado. El resultado es codigo ST ejecutable que produce derivaciones verificables.