Órganon — lenguaje natural → lógica formal
Playground interactivo: escribe en español, obtén la fórmula lógica y ejecútala en vivo — sin IA, sin base de datos.
Escribe un argumento en español. autologic lo formaliza a código lógico sin usar IA (NLP basado en reglas), y ST lo ejecuta con su motor lógico (SAT solver CDCL propio, derivaciones, validez, contramodelos). Todo el pipeline corre en vivo, en proceso, sin base de datos ni modelos de lenguaje.
Qué es interactivo
Todo el pipeline es en vivo. El texto que escribes se formaliza y se ejecuta en una funcion serverless de Vercel (runtime Node), llamando en proceso a las dos librerias. No hay respuestas pre-grabadas; cada peticion recorre el pipeline completo (~10 ms).
Cómo funciona por dentro
1. autologic.formalize() segmenta el texto, detecta ~200 marcadores discursivos y patrones de inferencia (modus ponens, silogismo hipotético, cuantificadores...), y emite código ST.
2. st-lang.evaluate() parsea y ejecuta ese codigo, devolviendo el estado logico de cada derivacion o verificacion (provable, satisfiable, refutable...).
Límites honestos
El formalizador es basado en reglas, no un LLM: brilla con argumentos estructurados (condicionales, silogismos, operadores modales/deónticos) y puede devolver indeterminado con prosa libre o correferencias ambiguas. Eso es por diseno: cero alucinacion, trazabilidad total.
ST — Symbolic Theory Language
Lenguaje ejecutable de lógica formal con 11 perfiles (proposicional, modal, deóntico, epistémico, intuicionista, temporal LTL, paraconsistente Belnap, aristotélico, probabilístico, aritmética y primer orden). El SAT solver CDCL es TypeScript puro con VSIDS, clause learning y reinicios Luby. Z3 se carga perezosamente solo si se necesita.
- Derivaciones, tablas de verdad, contramodelos, MUS
- Curry-Howard, System F, tipos dependientes (MLTT)
- Text Layer: vincular pasajes de documentos con fórmulas
- CLI, REPL, API programática (este playground la usa)
auto.logic — NLP → lógica sin IA
Formalizador NLP basado en reglas: stemmers Snowball, ~200 marcadores discursivos en español e inglés, detección de patrones de inferencia. Convierte oraciones a código ST sin modelos de lenguaje, sin APIs externas, con trazabilidad total de cada atom → texto fuente.
- Patrones: modus_ponens, modus_tollens, hypothetical_syllogism
- Cuantificadores: universal_generalization, universal_instantiation
- Operadores modales/deónticos/epistémicos detectados por marcadores
- 11 casos difíciles validados manualmente (jurídicos, filosóficos, matemáticos)