ST — Symbolic Theory Language
ST es un lenguaje ejecutable para logica formal, argumentacion y formalización documental. Combina un motor logico multi-perfil (11 sistemas logicos), un SAT solver CDCL propio, scripting imperativo y una Text Layer para conectar formulas con texto humano. Este playground lo expone via API en proceso, sin base de datos ni GPU.
1. Estructura minima de un script ST
Todo script ST comienza con una declaracion logic que selecciona el perfil logico 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 logicos (11 sistemas)
El perfil determina la semantica, los operadores disponibles y el motor de decision. Un mismo argumento puede producir resultados distintos segun el perfil.
| Perfil | Operadores clave | Uso tipico |
|---|---|---|
| classical.propositional | → & | ! ↔ ^ | Logica clasica, argumentacion basica |
| classical.first_order | ∀ ∃ predicados | Razonamiento sobre individuos y propiedades |
| modal.k | □ (necesario) ◇ (posible) | Mundos posibles, necesidad metafisica |
| deontic.standard | O (obligacion) P (permision) F (prohibicion) | Etica, normas juridicas, compliance |
| epistemic.s5 | K_a (sabe a) B_a (cree a) | Conocimiento, informacion multi-agente |
| intuitionistic.propositional | sin tercero excluido, sin doble negacion | Matematicas constructivas, tipos dependientes |
| temporal.ltl | X (next) U (until) G (always) F (eventually) | Verificacion de sistemas, protocolos |
| paraconsistent.belnap | 4 valores: T / F / B / N | Contradicciones sin explosion, bases de datos inconsistentes |
| aristotelian.syllogistic | todo / algun / ningun + predicados | Silogismos, razonamiento juridico clasico |
| probabilistic.basic | P(·) ∈ [0,1] redes Bayesianas | Inferencia probabilistica, incertidumbre |
| arithmetic | + * = < ≤ mod | Propiedades aritmeticas, divisibilidad |
3. Comandos de razonamiento
derive <meta> from {<premisas>}
Deriva una formula a partir de un conjunto explícito de premisas por nombre. Usa el motor de derivacion del perfil activo (resolucion, natural deduction, etc.).
axiom a1 : P -> Q
axiom a2 : P
derive Q from {a1, a2} // status: provableprove <formula>
Prueba una formula desde la teoria 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 formula es valida (tautologia) 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 formula.
check satisfiable (P & Q) // satisfacible check satisfiable (P & !P) // insatisfacible
check equivalent <f1>, <f2>
Compara equivalencia logica entre dos formulas (ambas tienen los mismos modelos).
check equivalent !(P & Q), (!P | !Q) // De Morgan: equivalente
countermodel <formula>
Busca un modelo (asignacion de valores de verdad) que falsifique la formula. Util para encontrar contra-ejemplos.
countermodel (P -> Q) // modelo: P=true, Q=false
4. Scripting: variables, funciones y teorias
ST incluye un lenguaje de scripting completo que permite nombrar formulas, encapsular logica en funciones y agrupar conocimiento en teorias 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. Logicas no clasicas — 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
Deontica — obligacion y prohibicion
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 evadirEpistemica 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
Aristotelica — 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 formulas formales y claims verificables. Es la caracteristica mas 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 — tecnologia interna
El nucleo 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 formula lo requiere explicitamente.
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. Cache de derivaciones con memoizacion y theorem-cache persistente por sesion.
MUS — Minimal Unsatisfiable Subsets
Diagnostica inconsistencias identificando el subconjunto minimo de clausulas que causan el conflicto. Util para depurar teorias.
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).
Logica lineal y π-calculo
Sublogicas estructurales (no-contraction, no-weakening), proof nets canonicos y razonamiento sobre procesos concurrentes.
Z3 como co-motor opcional
Para formulas fuera del alcance del CDCL nativo (QBF, aritmetica no lineal), ST carga z3-solver de forma perezosa via import() dinamico. El playground NO activa este camino.
8. API programatica (TypeScript)
Este playground usa directamente la API programatica de ST desde una funcion 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.