ST — Symbolic Theory Language
ST es un lenguaje ejecutable para lógica formal, argumentación y formalización documental. Combina un motor lógico multi-perfil (11 sistemas lógicos), un SAT solver CDCL propio, scripting imperativo y una Text Layer para conectar fórmulas con texto humano. Este playground lo expone vía API en proceso, sin base de datos ni GPU.
1. Estructura mínima de un script ST
Todo script ST comienza con una declaración logic que selecciona el perfil lógico activo. Luego se mezclan declaraciones (axiomas, teoremas, variables) con comandos ejecutables (derive, check, prove).
logic classical.propositional
axiom a1 : P -> Q
axiom a2 : P
derive Q from {a1, a2}
check valid (P | !P)La salida es estructurada: cada comando produce un resultado con status (provable, valid, satisfiable, etc.) que el playground muestra en el panel 3.
2. Perfiles lógicos (11 sistemas)
El perfil determina la semántica, los operadores disponibles y el motor de decisión. Un mismo argumento puede producir resultados distintos según el perfil.
| Perfil | Operadores clave | Uso típico |
|---|---|---|
| classical.propositional | → & | ! ↔ ^ | Lógica clásica, argumentación básica |
| classical.first_order | ∀ ∃ predicados | Razonamiento sobre individuos y propiedades |
| modal.k | □ (necesario) ◇ (posible) | Mundos posibles, necesidad metafísica |
| deontic.standard | O (obligación) P (permisión) F (prohibición) | Ética, normas jurídicas, compliance |
| epistemic.s5 | K_a (sabe a) B_a (cree a) | Conocimiento, información multi-agente |
| intuitionistic.propositional | sin tercero excluido, sin doble negación | Matemáticas constructivas, tipos dependientes |
| temporal.ltl | X (next) U (until) G (always) F (eventually) | Verificación de sistemas, protocolos |
| paraconsistent.belnap | 4 valores: T / F / B / N | Contradicciones sin explosión, bases de datos inconsistentes |
| aristotelian.syllogistic | todo / algún / ningún + predicados | Silogismos, razonamiento jurídico clásico |
| probabilistic.basic | P(·) ∈ [0,1] redes Bayesianas | Inferencia probabilística, incertidumbre |
| arithmetic | + * = < ≤ mod | Propiedades aritméticas, divisibilidad |
3. Comandos de razonamiento
derive <meta> from {<premisas>}
Deriva una fórmula a partir de un conjunto explícito de premisas por nombre. Usa el motor de derivación del perfil activo (resolución, natural deduction, etc.).
axiom a1 : P -> Q
axiom a2 : P
derive Q from {a1, a2} // status: provableprove <formula>
Prueba una fórmula desde la teoría acumulada (todos los axiomas declarados), sin lista explícita de premisas.
axiom a1 : P -> Q axiom a2 : P prove Q // status: provable
check valid <formula>
Verifica si la fórmula es válida (tautología) en el perfil activo. El SAT solver CDCL confirma que no hay modelo que la falsifique.
check valid (P | !P) // valido (tautologia) check valid (P -> Q) // invalido (hay contramodelo)
check satisfiable <formula>
Verifica si existe al menos un modelo que satisfaga la fórmula.
check satisfiable (P & Q) // satisfacible check satisfiable (P & !P) // insatisfacible
check equivalent <f1>, <f2>
Compara equivalencia lógica entre dos fórmulas (ambas tienen los mismos modelos).
check equivalent !(P & Q), (!P | !Q) // De Morgan: equivalente
countermodel <formula>
Busca un modelo (asignación de valores de verdad) que falsifique la fórmula. Útil para encontrar contra-ejemplos.
countermodel (P -> Q) // modelo: P=true, Q=false
4. Scripting: variables, funciones y teorías
ST incluye un lenguaje de scripting completo que permite nombrar fórmulas, encapsular lógica en funciones y agrupar conocimiento en teorías reutilizables.
logic classical.propositional
// Variables con etiqueta semantica
let regla = "Si estudio, apruebo" : (E -> A)
let hecho = "Estudio hoy" : E
// Derivar usando alias
derive A from {regla, hecho}
// Funcion reutilizable
fn revisar(X) {
check satisfiable X
return X
}
revisar((P -> Q))
// Teoria encapsulada
theory CursoLogica {
axiom base : E -> A
theorem identidad : (P -> P)
}
print CursoLogica.base5. Lógicas no clásicas — ejemplos
Modal K — necesidad y posibilidad
logic modal.k axiom ley_necesaria : □(L) // Es necesario que se cumplan las leyes axiom regla : □(L) -> ◇(S) // Si es necesario L, es posible sancionar prove ◇(S) // posible sancionar
Deóntica — obligación y prohibición
logic deontic.standard
axiom pagar : O(P) // Es obligatorio pagar impuestos
axiom regla : O(P) -> F(E) // Si obligatorio pagar, prohibido evadir
// F(x) = forbidden (prohibicion)
prove F(E) // prohibido evadirEpistémica S5 — conocimiento
logic epistemic.s5 // K_a(P) = el agente 'a' sabe que P axiom sabe_cerrado : K_juan(BANCO_CERRADO) axiom regla : K_juan(BANCO_CERRADO) -> !IRA_BANCO prove !IRA_BANCO // Juan no ira al banco
Aristotélica — silogismos
logic aristotelian.syllogistic // forall / exists como en primer orden axiom mayor : forall x (humano(x) -> mortal(x)) axiom menor : humano(socrates) prove mortal(socrates) // Modus Barbara
6. Text Layer — formalizar documentos
La Text Layer de ST permite vincular pasajes de documentos con fórmulas formales y claims verificables. Es la característica más avanzada del lenguaje: convierte un documento de texto en una base de conocimiento verificable.
logic classical.propositional
// Declarar pasajes de un documento filosofico
let p1 = passage([[kant-critica.md#prolegomenos]])
let p2 = passage([[kant-critica.md#estetica-trascendental]])
// Formalizar los pasajes como formulas
let f1 = formalize p1 as (I -> J) // Si hay intuicion pura → juicio sintetico a priori
let f2 = formalize p2 as (J -> G) // Si juicio sintetico a priori → geometria posible
// Claims con soporte y nivel de confianza
claim c1 = f1
claim c2 = f2
support c1 <- p1
support c2 <- p2
confidence c1 = 0.92
confidence c2 = 0.88
// Derivacion formal del argumento kantiano
axiom intuicion : I // Hay intuicion pura
axiom kant1 : I -> J
axiom kant2 : J -> G
derive G from {kant1, kant2, intuicion} // La geometria euclidiana es posible7. Motor SAT CDCL — tecnología interna
El núcleo de ST es un SAT solver CDCL (Conflict-Driven Clause Learning) escrito enteramente en TypeScript. No delega a Z3 ni a binarios externos para el caso base; Z3 se carga de forma perezosa solo si una fórmula lo requiere explícitamente.
CDCL con VSIDS
Conflict-Driven Clause Learning con heuristica VSIDS (Variable State Independent Decaying Sum) para seleccion de variables. Reinicios tipo Luby para evitar estancamientos.
SAT incremental
Reutiliza el estado del solver entre consultas dentro del mismo script. Caché de derivaciones con memoización y theorem-cache persistente por sesión.
MUS — Minimal Unsatisfiable Subsets
Diagnostica inconsistencias identificando el subconjunto mínimo de cláusulas que causan el conflicto. Útil para depurar teorías.
Curry-Howard (type theory)
Pruebas como programas: System F con polimorfismo parametrico, MLTT (Martin-Löf Type Theory), tipos dependientes y NbE (Normalizacion por Evaluacion).
Lógica lineal y π-cálculo
Sublógicas estructurales (no-contraction, no-weakening), proof nets canónicos y razonamiento sobre procesos concurrentes.
Z3 como co-motor opcional
Para fórmulas fuera del alcance del CDCL nativo (QBF, aritmética no lineal), ST carga z3-solver de forma perezosa vía import() dinámico. El playground NO activa este camino.
8. API programática (TypeScript)
Este playground usa directamente la API programática de ST desde una función serverless de Vercel (runtime Node). No hay procesos hijos ni subshells.
import { evaluate, type STEvalResult } from '@stevenvo780/st-lang/api';
const source = `
logic classical.propositional
axiom a1 : P -> Q
axiom a2 : P
derive Q from {a1, a2}
`;
const result: STEvalResult = evaluate(source);
// result.results[0].status === 'provable'
// result.exitCode === 0
// result.stdout contiene la salida del interpreteEl tipo STEvalResult expone ok, exitCode, stdout, stderr, results (array de resultados estructurados) y diagnostics.