Ó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 espanol. autologic lo formaliza a codigo logico sin usar IA (NLP basado en reglas), y ST lo ejecuta con su motor logico (SAT solver CDCL propio, derivaciones, validez, contramodelos). Todo el pipeline corre en vivo, en proceso, sin base de datos ni modelos de lenguaje.
Que 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).
Como funciona por dentro
1. autologic.formalize() segmenta el texto, detecta ~200 marcadores discursivos y patrones de inferencia (modus ponens, silogismo hipotetico, cuantificadores...), y emite codigo ST.
2. st-lang.evaluate() parsea y ejecuta ese codigo, devolviendo el estado logico de cada derivacion o verificacion (provable, satisfiable, refutable...).
Limites honestos
El formalizador es basado en reglas, no un LLM: brilla con argumentos estructurados (condicionales, silogismos, operadores modales/deonticos) 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 logica formal con 11 perfiles (proposicional, modal, deontico, epistemico, intuicionista, temporal LTL, paraconsistente Belnap, aristotelico, probabilistico, aritmetica 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 formulas
- CLI, REPL, API programatica (este playground la usa)
auto.logic — NLP → logica sin IA
Formalizador NLP basado en reglas: stemmers Snowball, ~200 marcadores discursivos en espanol e ingles, deteccion de patrones de inferencia. Convierte oraciones a codigo 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/deonticos/epistemicos detectados por marcadores
- 11 casos dificiles validados manualmente (juridicos, filosoficos, matematicos)