ST ya no es solo un lenguaje declarativo para lógica formal: es un lenguaje ejecutable para enseñar, verificar, explorar y guionar razonamientos. Permite definir axiomas, teoremas, variables, bloques de prueba, teorías singleton, teorías-clase parametrizadas, funciones, módulos y comandos de verificación (validez, satisfacibilidad, equivalencia, derivación, tablas de verdad, análisis y explicación) sobre 11 perfiles distintos, desde la clásica proposicional hasta la probabilística y la aritmética. El runtime actual también incluye import/export selectivo, operadores extendidos (xor, nand, nor) y helpers nativos para inspección, metalógica, render formal y automatización.
Cada perfil implementa un motor semántico propio (tablas de verdad, tableaux analíticos, modelos Kripke, retículos de 4 valores, cálculo probabilístico, evaluación aritmética o validación silogística directa). Además, el runtime real soporta let, set, print, if, for, while, fn, theory, import, export,analyze, explain,render, typeof,is_valid, get_atoms, modos de verbosidad, detección de 10 falacias, warnings de paradoja y exportación formal en LaTeX.
Lenguaje, diseño conceptual y documentación base: Steven Vallejo Ortiz. Esta edición del manual corrige la semántica real de variables, funciones, clases con theory, condicionales, módulos, metalógica y límites del runtime.
/docs/st queda como índice central del lenguaje: sintaxis, comandos, runtime real, metalógica, laboratorio y anexos técnicos.
Cada sistema tiene ahora una página dedicada en /docs/st/[slug]para estudiar un perfil completo sin mezclarlo con los demás.
Cada guía apunta a un único .st completo por perfil, validado contra el motor real del paquete.
1. Usa esta página para entender el lenguaje, el runtime y las capacidades comunes.
2. Entra a una guía por lógica cuando quieras estudiar un sistema completo de principio a fin.
3. Descarga el script del perfil y compáralo con la salida inline del editor embebido.
La escuela queda ordenada como un índice de guías por lógica. Esta portada resume y agrupa cada sistema; el detalle completo queda en su página dedicada.
Empieza por la lógica clásica proposicional y luego sube a primer orden. Estas dos guías sostienen el resto de la escuela.
Aprender a leer, construir y verificar fórmulas con conectivos clásicos.
Es la puerta de entrada a todo ST. Aquí estudias proposiciones atómicas, tablas de verdad, tautologías, contradicciones, contingencias y reglas básicas de derivación.
truth_tablecheck validcheck satisfiablecheck equivalentPasar de proposiciones globales a estructuras con individuos, propiedades y cuantificadores.
FOL permite decir “todos”, “alguno”, “este individuo” y expresar relaciones entre objetos. Es la base para modelar conocimiento más rico que P o Q.
check validcheck satisfiablederivecountermodelReúne los perfiles basados en mundos posibles, accesibilidad, obligación, conocimiento y evolución temporal.
Entender necesidad y posibilidad usando mundos posibles.
La lógica modal agrega una idea crucial: una fórmula puede no depender solo del mundo actual, sino también de qué ocurre en mundos accesibles.
check validcheck satisfiablecheck equivalentcountermodelModelar obligación, permiso y prohibición.
La lógica deóntica traduce reglas normativas: lo que debe hacerse, lo que está permitido y lo que está prohibido.
check validcheck satisfiablederivecountermodelDistinguir verdad, conocimiento y accesibilidad epistémica.
Aquí las fórmulas hablan de lo que un agente sabe o considera posible. S5 modela conocimiento idealizado con accesibilidad universal.
check validcheck satisfiablederiveRazonar sobre estados presentes y futuros.
La lógica temporal permite expresar propiedades que deben mantenerse siempre, ocurrir eventualmente o suceder en el siguiente paso.
check validcheck satisfiablecheck equivalentderiveAquí quedan las lógicas que corrigen o extienden intuiciones clásicas: constructividad, paraconsistencia y probabilidad.
Estudiar una noción constructiva de verdad.
En lógica intuicionista, “verdadero” significa “constructivamente demostrable”. Por eso no todo principio clásico se conserva.
check validcheck satisfiablecheck equivalentcountermodelRazonar con inconsistencia sin explosión trivial.
Belnap introduce cuatro valores: verdadero, falso, ambos y ninguno. Permite describir bases de datos incompletas o contradictorias sin colapso lógico.
check validcheck satisfiablecheck equivalentcountermodelMedir la fuerza probabilística de fórmulas clásicas.
En lugar de evaluar solo verdad o falsedad, este perfil calcula probabilidades de fórmulas sobre distribuciones discretas de probabilidad.
check validcheck satisfiablecheck equivalenttruth_tablePerfiles para programación explicativa, razonamiento numérico y tradición silogística.
Usar ST como lenguaje explicativo con números, comparaciones, variables, loops y funciones.
El perfil arithmetic muestra con claridad que ST ya es un lenguaje ejecutable completo para docencia y prototipado. Aquí se mezclan cálculo, control de flujo, funciones, explain y scripting visible paso a paso.
check validcheck satisfiableexplaincountermodelEntender los modos silogísticos categóricos clásicos.
Este curso traduce la lógica de términos de Aristóteles a ST: universal afirmativa, universal negativa, particular afirmativa y particular negativa.
check validcheck satisfiablederivelogic classical.propositionalObligatorio para activar un perfil. Si vuelves a declarar logic más abajo, ST cambia el perfil activo desde ese punto.
logic classical.propositional
check valid (P | !P)
logic arithmetic
check valid (2 + 3) >= 5Los tests del runtime confirman que puedes mezclar secciones con distintos perfiles en un mismo script, siempre declarando logic antes de cada bloque.
axiom modus : P -> Q
axiom base = PSe aceptan tanto : como = para la asignación.
theorem resultado : QLos teoremas representan consecuencias que se desean conservar.
assume h1 : P -> Q
assume h2 : P
show Q
derive Q from {h1, h2}
qedLas hipótesis son temporales, el runtime comprueba la meta y registra un teorema interno si la prueba cierra.
let regla = "Si estudio, apruebo" : (E -> A)
let hecho = E
print regla
set hecho = A
render theoryCuando let recibe una fórmula, ST la registra como alias reutilizable y también como axioma implícito de la teoría actual.
set verbose = on
set verbose = proof
set verbose = model
set verbose = off
set output = latexverbose es una variable de control del runtime: on expande notas y comparación entre sistemas; proof y model enfocan el detalle; output=latex exporta árboles de prueba en formato formal cuando la operación genera prueba.
if valid (P | !P) {
print "tautología"
} else if satisfiable P {
print "contingencia"
} else {
print "contradicción"
}
for F in { P, Q, (R -> R) } {
print F
}
while satisfiable estado {
set estado = P & !P
}ST soporta if, else if, else, for y while sobre condiciones lógicas reales: valid, invalid, satisfiable y unsatisfiable.
fn identidad(X) {
return X
}
check valid identidad((P -> P))
print get_atoms(identidad((P -> Q) & R))En ST 4.14.0 las llamadas a función también pueden reutilizarse dentro de otros comandos si la función ya fue declarada.
theory Base {
let ley = P -> Q
}
theory Caja(valor) {
let dato = valor
fn ver() {
print dato
}
}
print Base.ley
let caja = Caja("demo")
print caja.dato
caja.ver()Una theory sin parámetros se instancia al declararse; una theory con parámetros actúa como plantilla de clase.
// utilidades.st
export let Ley = P -> P
export fn revisar(X) {
return X
}
// curso.st
import "utilidades.st"
check valid Ley
print typeof(revisar((P -> Q)))La importación solo fusiona los símbolos marcados con export y mantiene el archivo importado aislado del scope consumidor.
// comentario de línea
/* comentario de bloque */
axiom mezcla = P | Q & R
axiom cadena = P -> Q -> R
support c1 <- p1El lexer ignora // y /* ... */. Además, & tiene mayor precedencia que |, la implicación asocia a la derecha y support usa <-.
!P // negación
P & Q // conjunción
P | Q // disyunción
P -> Q // implicación material
P <-> Q // bicondicionalP ^ Q // XOR
P ⊕ Q // XOR unicode
P !& Q // NAND
P ↑ Q // NAND unicode
P !| Q // NOR
P ↓ Q // NOR unicodeEl lexer real acepta tanto formas ASCII como Unicode para XOR, NAND y NOR.
forall x (P(x) -> Q(x))
exists x (P(x) & R(x))Solo disponibles en classical.first_order y aristotelian.syllogistic.
2 + 3 * 4
(2 + 3) * 4
2 + 3 < 10
print typeof(2)
print typeof("hola")
print typeof((P -> Q))Arithmetic agrega operadores numéricos y comparaciones; typeof distingue Number, String y Formula.
[](P) / K(P) / O(P) / G(P) // necesidad, conocimiento, obligación, siempre
<>(P) / B(P) / P(P) / F(P) // posibilidad, creencia, permisión, eventualmente
F(P) // prohibición deóntica = [](!P)
X(P) / next P / siguiente P
(P until Q) / (P hasta Q)K/B solo se leen como modalidades en epistemic.s5; O/P/F en deontic.standard; G/F y next/until en temporal.ltl. Fuera de esos perfiles, nombres como K(P) siguen siendo predicados normales.
logica classical.propositional
axioma regla = P -> Q
sea hecho = P
derivar Q desde {regla, hecho}
si valido (P -> P) {
imprimir "ok"
}La sintaxis en español no se limita al glosario: el parser cubre comandos, scripting, teorías, Text Layer, import/export y pruebas estructuradas.
print is_valid(P -> P)
print is_satisfiable(P & Q)
print get_atoms((P -> Q) & R)
let nombre = input("Nombre:")Estas funciones nativas existen en el runtime real. input está orientado a CLI/REPL y las respuestas meta salen como strings legibles.
check valid <φ>Verifica si la fórmula es válida en la lógica activa; con verbose puede identificar axiomas, clasificaciones, comparación entre sistemas y traza del tableau.
logic classical.propositional
set verbose = on
check valid (P -> (Q -> P))check satisfiable <φ>Comprueba si existe al menos un modelo donde φ es verdadera; en perfiles modales, epistémicos y temporales puede mostrar contramodelos Kripke detallados.
logic epistemic.s5
set verbose = model
check satisfiable (P & ![]P)check equivalent <φ>, <ψ>Determina si dos fórmulas son lógicamente equivalentes.
check equivalent !(P & Q), (!P | !Q)derive <meta> from {<premisas>}Intenta demostrar la meta a partir de las premisas listadas y, en el runtime nuevo, nombra el patrón de razonamiento, el esquema y la prueba paso a paso.
logic classical.propositional
set verbose = proof
axiom regla : P -> Q
axiom base = P
derive Q from {regla, base}prove <meta> from {<axiomas>}Similar a derive, pero verifica contra la teoría registrada.
logic classical.propositional
axiom modus : P -> Q
axiom base = P
prove Q from {modus, base}countermodel <φ>Si φ no es válida, muestra un modelo que la falsifica; en clásica marca la valuación crítica y en perfiles Kripke muestra mundos, accesibilidad y valuación.
logic modal.k
set verbose = model
countermodel ([]P -> P)truth_table <φ>Genera la tabla de verdad en formato Markdown (máx. 20 variables).
truth_table P -> (Q -> P)analyze {<premisas>} -> <conclusión>Evalúa una inferencia completa y detecta falacias formales conocidas. El runtime activo registra diez detectores explícitos.
logic classical.propositional
analyze {P, P -> Q} -> Q
analyze {P -> Q, Q} -> P
analyze {P -> Q, !P} -> !Qexplain <φ>Explica una fórmula según el perfil activo. En proposicional ya incluye sub-fórmulas, formas normales, cláusulas, completitud funcional y esquemas algebraicos; en otros perfiles despliega marcos, paradojas, patrones o cálculo paso a paso.
logic classical.propositional
set verbose = on
explain (P -> Q)render <target>Renderiza teoría, claims o elementos específicos del estado actual.
logic classical.propositional
axiom a1 : P -> Q
render theoryrefute <φ>Alias directo de countermodel para refutar una fórmula.
refute P -> Qst run <archivo.st>Ejecuta un script completo desde CLI.
st run teoria.stst check <archivo.st>Valida sintaxis, warnings y resultados negativos relevantes sin abrir el editor.
st check teoria.stst eval "<expresión>"Evalúa una expresión rápida; si no declaras logic, asume classical.propositional.
st eval "check valid (P -> P)"st profilesLista los perfiles lógicos disponibles desde la CLI real actual.
st profilesst repl / st protocolAbre el REPL interactivo o el modo JSON-RPC para integración con editores.
st repl
st protocolset verbose = on|off|proof|modelControla la riqueza pedagógica de la salida del runtime usando la sintaxis real de set.
logic classical.propositional
set verbose = on
check valid (P -> (Q -> P))set output = latexCuando una operación genera prueba formal, cambia la salida del árbol a formato LaTeX.
logic classical.propositional
set verbose = proof
set output = latex
axiom regla = P -> Q
axiom base = P
derive Q from {regla, base}:profiles / :profile / :theory / :claims / :resetMetacomandos disponibles dentro del REPL para inspeccionar el estado del intérprete.
st repl
:profiles
:profile
:theory
:claims
:resetEl salto más grande del runtime nuevo no es solo lógico sino didáctico: muchas operaciones ahora devuelven clasificación, esquema, notas educativas, trazas y comparaciones que antes había que explicar fuera del motor.
El motor nuevo usa una variable de control para alternar entre salida compacta, salida total, foco en prueba y foco en modelo. La sintaxis real es con set, no con un comando aparte.
logic classical.propositional
set verbose = on
check valid (P -> (Q -> P))
set verbose = proof
set output = latex
axiom regla = P -> Q
axiom base = P
derive Q from {regla, base}on abre comparación entre sistemas, notas pedagógicas y trazas; proof concentra pasos de prueba; model prioriza modelos y contramodelos; output=latex emite árboles de prueba formales.
En proposicional, explain ya no se limita a decir si algo es tautológico o contingente. Puede desplegar conectivo principal, profundidad, sub-fórmulas, formas normales, cláusulas para resolución, completitud funcional y esquemas algebraicos.
logic classical.propositional
set verbose = on
explain (P -> Q)Cada perfil especializa explain: FOL agrega prenex y Skolem; temporal clasifica patrones; Belnap dibuja el retículo; probabilística explica el cálculo paso a paso.
El análisis de inferencias ya no se queda en dos casos básicos. El runtime activo cubre afirmación del consecuente, negación del antecedente, medio no distribuido, composición, falso dilema, petición de principio, conversión ilícita, generalización apresurada, cuaternio terminorum y división.
logic classical.propositional
analyze {P -> Q, Q} -> P
analyze {P -> Q, !P} -> !QLa salida incluye nombre de la falacia, explicación breve y patrón lógico. El changelog habla de once, pero el detector activo del runtime hoy expone diez checks registrados.
Los checks con verbose pueden contrastar una misma fórmula entre perfiles compatibles y mostrar tableaux o contramodelos Kripke cuando el sistema lo soporta.
logic deontic.standard
set verbose = on
check valid ([]P -> [](P | Q))Esta salida puede incluir identificación de axioma o paradoja, comparación cruzada y traza del tableau. En modal, deóntica, epistémica y temporal aparecen además mundos y accesibilidad.
Esta sección documenta el comportamiento real del runtime, no una intención futura del lenguaje. Está contrastada con @stevenvo780/st-lang v4.14.0y corrige varios puntos que antes estaban simplificados u obsoletos.
La verbosidad y el formato de prueba no son comandos mágicos separados: el runtime los lee desde variables del estado actual, por eso la sintaxis real es set verbose = ... y set output = ....
logic classical.propositional
set verbose = proof
set output = latex
axiom regla = P -> Q
axiom base = P
derive Q from {regla, base}El changelog interno habla de un “sistema de verbosidad”; en la sintaxis real actual se controla con set sobre verbose y output.
Cuando let recibe una fórmula, ST registra un alias reutilizable y además lo incorpora como axioma implícito de la teoría actual. Cuando recibe solo texto, conserva una descripción semántica para explicaciones, modelos y contramodelos.
logic classical.propositional
let regla = "Si estudio, apruebo" : (E -> A)
let hecho = E
derive A from {regla, hecho}
render theoryPor eso derive, prove, render y countermodel pueden reutilizar let como si fueran premisas con nombre.
Una theory sin parámetros es un singleton instanciado al declararse; una theory con parámetros es una plantilla de clase que se instancia al llamarla como función. Los métodos usan notación con punto y los miembros privados no salen del scope.
logic classical.propositional
theory Base {
let ley = P -> Q
}
theory Caja(valor) {
let dato = valor
fn ver() {
print dato
}
}
print Base.ley
let caja = Caja("demo")
print caja.dato
caja.ver()La herencia con extends hoy funciona contra una teoría padre ya instanciada, normalmente un singleton.
Las funciones restauran los bindings previos al terminar, aceptan varios parámetros y pueden aparecer dentro de otras fórmulas o comandos si ya están declaradas y devuelven una fórmula utilizable.
logic classical.propositional
fn identidad(X) {
return X
}
check valid identidad((P -> P))
print get_atoms(identidad((P -> Q) & R))Esto corrige una documentación anterior: en el runtime real sí puedes reutilizar llamadas de función dentro de expresiones conocidas por el parser.
import carga un archivo en un scope aislado, ejecuta solo declaraciones exportadas y luego fusiona exclusivamente los símbolos marcados con export.
// utilidades.st
export let Ley = P -> P
export fn revisar(X) {
return X
}
// curso.st
import "utilidades.st"
check valid Ley
print typeof(revisar((P -> Q)))Ese encapsulamiento evita contaminar el script importador con variables internas o salidas accidentales.
La auditoría final contra lexer, parser y tests confirma detalles sintácticos que antes quedaban implícitos o dispersos.
logic classical.propositional
// bloque clásico
check valid (P | Q & R) -> (P | (Q & R))
logic arithmetic
/* bloque aritmético */
check valid (2 + 3) >= 5Los aliases K/B/O/F/G son contextuales: en perfiles no modales, formas como K(P) vuelven a ser predicados ordinarios.
for restaura el binding previo de la variable iterada cuando termina. while reevalúa una condición lógica en cada vuelta y corta a las 1000 iteraciones con advertencia.
logic classical.propositional
set estado = P
while satisfiable estado {
print "iteración"
set estado = P & !P
}La mutación explícita es parte del modelo de ejecución: la condición se recalcula contra el estado lógico actualizado.
El runtime ya adjunta a muchos resultados metadatos útiles para docencia: patrón de razonamiento, esquema, clasificación de fórmula, formas normales, comparación entre perfiles, notas educativas, warnings de paradoja y traza del tableau.
logic deontic.standard
set verbose = on
check valid ([]P -> [](P | Q))No todos los perfiles llenan todos los campos, pero el núcleo ya está preparado para una salida mucho más rica que la de la documentación vieja.
ST ahora permite construir lecciones ejecutables y pequeños laboratorios con estado visible. La idea no es competir con un lenguaje generalista, sino dar una capa de programación explicativa alrededor del razonamiento formal. La diferencia importante es que aquí el flujo del programa depende de propiedades lógicas reales del contenido que estás enseñando.
Usa let para nombrar fórmulas o descripciones y set para mutar una variable durante el script. Un let con fórmula también queda disponible para derive y prove.
logic classical.propositional
let regla = "Si estudio, apruebo" : (E -> A)
let hecho = E
derive A from {regla, hecho}
set hecho = A
print hecho
render theoryLas condiciones se evalúan con estatus lógicos reales: valid, invalid, satisfiable o unsatisfiable.
logic classical.propositional
set estado = P
if valid (P | !P) {
print "tautología"
} else if satisfiable P {
print "contingencia"
} else {
print "contradicción"
}
for Caso in { P, Q, (R -> R) } {
print Caso
}
while satisfiable estado {
print "iteración"
set estado = P & !P
}Las funciones encapsulan pasos repetibles, return corta la ejecución del cuerpo y la llamada puede volver a usarse dentro de otros comandos si devuelve una fórmula.
logic classical.propositional
fn revisar(X) {
explain X
return X
}
check valid revisar((P -> P))
print get_atoms(revisar((P -> Q) & R))Los archivos importados solo exponen lo que marques con export. Eso permite modularizar sin contaminar el scope.
// utilidades.st
export let Ley = P -> P
export fn revisar(X) {
return X
}
// curso.st
import "utilidades.st"
check valid Ley
print typeof(revisar((P -> Q)))Una theory sin parámetros actúa como singleton; con parámetros actúa como clase instanciable. extends reutiliza miembros públicos de una teoría padre ya instanciada.
logic classical.propositional
theory Base {
let ley = P -> Q
}
theory Hija extends Base {
fn ver() {
print ley
}
}
theory Caja(valor) {
let dato = valor
}
print Hija.ley
let caja = Caja("demo")
print caja.dato
Hija.ver()El intérprete incluye helpers ya listos para inspección, validación rápida, extracción de átomos y entrada interactiva.
logic arithmetic
print typeof(2)
print typeof("hola")
print typeof((P -> Q))
print is_valid(2 + 3 < 10)
print is_satisfiable(5 > 3)
print get_atoms((P -> Q) & R)
let nombre = input("Nombre:")ST sí soporta meta lógica operativa: puedes escribir teoría sobre teorías, clases que inspeccionan fórmulas, módulos que auditan inferencias y rutinas que consultan la semántica del perfil activo mediante typeof, get_atoms,is_valid, is_satisfiable,analyze y explain.
Usa theory Meta(nombre) como clase instanciable. Cada instancia puede clasificar una fórmula, extraer sus átomos y pedir una explicación formal del motor.
logic classical.propositional
theory Meta(nombre) {
let etiqueta = nombre
fn inspeccionar(F) {
print etiqueta
print typeof(F)
print get_atoms(F)
print is_valid(F)
print is_satisfiable(F)
explain F
return F
}
fn clasificar(F) {
if valid F {
print "tautologia"
} else if satisfiable F {
print "contingente"
} else {
print "contradiccion"
}
return F
}
}
let meta = Meta("Meta")
meta.inspeccionar((P -> (Q -> P)))
meta.clasificar((P & !P))La metalógica en ST no requiere una keyword especial: se construye combinando theory, fn, typeof, get_atoms, is_valid, is_satisfiable, if y explain.
La metalógica no se limita a fórmulas sueltas. También puede auditar inferencias, detectar falacias y convertir una teoría en un objeto de inspección.
logic classical.propositional
theory MetaInferencia {
fn auditar() {
analyze {P, P -> Q} -> Q
analyze {P} -> Q
}
}
MetaInferencia.auditar()Aquí ST razona sobre la estructura del argumento, no solo sobre una proposición aislada.
Puedes encapsular rutinas metateóricas en un módulo exportable para reutilizarlas en cursos, pruebas internas o material pedagógico compartido.
// meta.st
export theory BibliotecaMeta {
let identidad = P -> P
fn auditar() {
print typeof(identidad)
print get_atoms(identidad)
check valid identidad
}
}
// curso.st
import "meta.st"
BibliotecaMeta.auditar()La clave es que import solo trae exports, así que la biblioteca metateórica queda limpia y controlada.
La documentación no solo cubre la sintaxis ST. También documenta el paquete que usa el frontend: desde ahí puedes ejecutar scripts, renderizar fórmulas en Unicode o LaTeX y conectar el motor con tus propias herramientas.
El frontend ya consume el paquete oficial. Puedes crear un intérprete, ejecutar un script y reutilizar la salida para paneles, laboratorios o integraciones pedagógicas.
import { createInterpreter } from '@stevenvo780/st-lang';
const interpreter = createInterpreter();
const result = interpreter.exec(`logic classical.propositional
set verbose = on
check valid (P -> (Q -> P))
`);
console.log(result.stdout);Esta es la misma ruta que usan los bloques ejecutables de la documentación.
El paquete actual expone helpers públicos para Unicode, LaTeX y detección programática de falacias. Los árboles de prueba en LaTeX se obtienen desde ST con set output = latex.
import { parse, formulaToUnicode, formulaToLaTeX, detectFallacies } from '@stevenvo780/st-lang';
const parsed = parse('logic classical.propositional\nclaim demo = P -> (Q -> P)');
if (parsed.ok) {
const claim = parsed.program.statements[1];
if (claim.kind === 'claim_decl') {
console.log(formulaToUnicode(claim.formula));
console.log(formulaToLaTeX(claim.formula));
}
}
console.log(detectFallacies);formulaToUnicode y formulaToLaTeX forman parte de la API pública del paquete actual. La exportación de pruebas completas se activa dentro del lenguaje con output=latex.
Todos los snippets ejecutables de esta página ahora pueden correrse inline. Además, este laboratorio deja un editor ST desplegado dentro de la documentación para que el lector modifique el ejemplo, lo ejecute al instante y compare la salida sin salir del manual.
Usa el botón Ejecutar o Ctrl/Cmd + Enter cuando el editor esté abierto.
Una de las mejores maneras de enseñar ST es tomar fragmentos filosóficos reales y traducirlos a una estructura ejecutable. En estos ejemplos usamoslet, descripciones semánticas, derivación, analyze, explain, condiciones y render para que el lector vea no solo la fórmula, sino el recorrido pedagógico.
Es una formalización excelente para introducir contradicción, negación y validez universal en proposicional.
logic classical.propositional
let P = "La misma cosa se afirma del mismo sujeto"
let principio = "No es posible afirmar y negar lo mismo al mismo tiempo" : !(P & !P)
print principio
check valid !(P & !P)
explain !(P & !P)
analyze {!(P & !P)} -> !(P & !P)Aquí usamos una letra proposicional con descripción semántica y una formalización muy cercana al corazón del texto filosófico.
Aunque el cogito completo rebasa la proposicional pura, una versión mínima sirve para enseñar dependencia inferencial y pasos explicativos.
logic classical.propositional
let P = "Pienso"
let E = "Existo"
let regla = "Si pienso, existo" : (P -> E)
let hecho = "Estoy pensando" : P
derive E from {regla, hecho}
analyze {P, P -> E} -> E
explain (P -> E)
render theoryNo pretende capturar toda la riqueza filosófica del cogito, sino mostrar cómo ST permite convertir un fragmento argumental en un guion verificable.
Sirve para modelar una inferencia práctica sencilla con variables descriptivas y control pedagógico del script.
logic classical.propositional
let D = "Algo depende de nosotros"
let T = "Debe trabajarse interiormente"
let regla = "Si depende de nosotros, debe trabajarse interiormente" : (D -> T)
let caso = "Este juicio depende de nosotros" : D
derive T from {regla, caso}
if valid (D -> D) {
print "la estructura base es coherente"
}
analyze {D, D -> T} -> TAquí el valor didáctico está en mezclar descripción, derivación e inferencia práctica sin perder claridad.
Aunque Kant se trabaja mejor en deóntica, una versión proposicional mínima ayuda a explicar traducción de lenguaje natural a estructura inferencial.
logic classical.propositional
let U = "La máxima puede universalizarse"
let M = "La acción es moralmente admisible"
let principio = "Si la máxima puede universalizarse, la acción es admisible" : (U -> M)
let caso = "Esta máxima puede universalizarse" : U
derive M from {principio, caso}
check equivalent (U -> M), (!U | M)
explain (U -> M)Este patrón ayuda a mostrar cómo una regla ética se vuelve una implicación formal sin agotar todo el contenido filosófico.
Este glosario resume las keywords más importantes del lenguaje y para qué sirven. Incluye la forma principal en inglés y, cuando existe, su alias en español. La idea es que puedas leer un script ST como si fuera una gramática viva del lenguaje.
Cada perfil activa un motor semántico específico. Haz clic en un perfil para ver su manual completo con semántica, operadores, axiomas, ejemplos válidos e inválidos, y limitaciones del motor.
El Text Layer extiende ST para vincular lógica formal con documentos en lenguaje natural. Permite formalizar pasajes, declarar claims verificables y agregar metadatos de soporte, confianza y contexto. El runtime renderizaclaims, theory y all.
let p1 = passage([[doc.md#clause-1]])Referencia a un ancla de documento externo.
let f1 = formalize p1 as (P & Q)Mapea el pasaje a una fórmula lógica.
claim c1 = f1Declara un claim verificable a partir de la formalización.
render claims
render theory
render allUsa render para inspeccionar claims, confianza, soporte, contexto y teoría compilada.
support c1 <- p1
confidence c1 = 0.85
context c1 = "Cláusula de privacidad del contrato"
render claimsST es un motor educativo y de prototipado. A continuación las limitaciones técnicas verificadas contra el motor real:
Cada ejemplo de esta documentación se valida automáticamente contra el motor ST real. El script npm run validate:st-docs ejecuta todos los archivos .st de la carpeta de descargas y verifica que el motor no lance errores.
npm run validate:st-docs\n# Ejecuta los 13 scripts .st canónicos contra @stevenvo780/st-lang\n# Salida esperada: ejecución completa sin erroresContexto listo para copiar y pegar en cualquier chat o workspace con IA. Incluye sintaxis completa, todos los perfiles, operadores, alias en español, API y referencias a secciones de la documentación.
# Prompt de contexto: Lenguaje ST
> Copia y pega este archivo como contexto en cualquier workspace o chat con IA para que el asistente sepa cómo usar el lenguaje ST.
---
## Qué es ST
**ST** (Symbolic Theory Language) es un lenguaje ejecutable para lógica formal, argumentación y formalización de documentos. Combina tres capas:
1. **Lógica formal**: axiomas, teoremas, derivaciones, validez, satisfacibilidad, contramodelos.
2. **Scripting declarativo**: variables, condicionales, loops, funciones, módulos, POO.
3. **Text Layer**: vincula pasajes de documentos con formalizaciones verificables.
Los archivos tienen extensión `.st` y se ejecutan con el CLI `st`.
**Documentación completa:**
- Manual local: `ST/DOCS.md` (secciones 1–20)
- Quickstart: `ST/QUICKSTART.md`
- README con sintaxis resumida: `ST/README.md`
---
## Instalación
```bash
# npm global
npm install -g @stevenvo780/st-lang
# o binario Linux
chmod +x st && sudo mv st /usr/local/bin/
```
---
## CLI principal
```bash
st run archivo.st # ejecutar archivo
st archivo.st # modo legacy
st check archivo.st # validar sintaxis
st run archivo.st --diagnostics # guardar diagnósticos JSON
st eval "check valid (P -> P)" # expresión rápida
st repl # modo interactivo
st profiles # listar perfiles disponibles
st protocol # protocolo para editores (LSP)
```
---
## Estructura mínima de un script
Todo script necesita declarar un perfil lógico al inicio:
```st
logic classical.propositional
axiom a1 : P -> Q
axiom a2 : P
derive Q from {a1, a2}
check valid (P | !P)
```
---
## Perfiles lógicos disponibles
| Perfil | Uso principal |
|---|---|
| `classical.propositional` | Lógica proposicional clásica (el más completo) |
| `classical.first_order` | Lógica de primer orden con cuantificadores |
| `modal.k` | Lógica modal (`[]` necesidad, `<>` posibilidad) |
| `deontic.standard` | Razonamiento normativo/deóntico |
| `epistemic.s5` | Razonamiento sobre conocimiento |
| `aristotelian.syllogistic` | Silogística aristotélica |
| `intuitionistic.propositional` | Sin tercero excluido |
| `temporal.ltl` | Lógica temporal (`next`, `until`) |
| `probabilistic.basic` | Razonamiento probabilístico básico |
| `paraconsistent.belnap` | Tolerante a inconsistencia |
| `arithmetic` | Aritmética explicable (`+`, `-`, `*`, `/`, `%`, `<`, `>`) |
Selección:
```st
logic modal.k
logic arithmetic
```
---
## Statements principales
### Núcleo lógico
```st
logic classical.propositional
axiom a1 : P -> Q -- declara axioma
theorem t1 : (P -> P) -- registra teorema
derive Q from {a1, a2} -- deriva desde premisas nombradas
prove (P -> P) -- prueba desde teoría acumulada
check valid (P | !P) -- verifica validez
check satisfiable (P & Q) -- verifica satisfacibilidad
check equivalent (!(P&Q)), (!P|!Q) -- equivalencia
truth_table (P -> Q) -- tabla de verdad
countermodel (P -> Q) -- busca contraejemplo
analyze {P, P->Q} -> Q -- evalúa inferencia + detecta falacias
explain (P & !P) -- explica fórmula en el perfil activo
render theory -- inspecciona teoría cargada
render claims -- inspecciona claims
```
Falacias detectadas por `analyze`: afirmación del consecuente, negación del antecedente, medio no distribuido.
### Variables y scripting
```st
let regla = P -> Q -- alias de fórmula (también como axioma implícito)
let causa = "Si llueve, se moja" : (L->M) -- descripción + fórmula
let P = "Llueve" -- descripción semántica de átomo
set regla = Q -> R -- reasignación mutable
print "texto" -- imprime texto
print regla -- imprime variable resuelta
```
### Control de flujo
```st
if valid (P | !P) {
print "tautología"
} else if satisfiable P {
print "satisfacible"
} else {
print "insatisfacible"
}
for F in { P, Q, (R -> R) } {
check valid F
}
set cond = P
while satisfiable cond {
print "iteración"
set cond = P & !P
}
```
Condiciones para `if`/`while`: `valid`, `invalid`, `satisfiable`, `unsatisfiable`.
Límite de seguridad en `while`: 1000 iteraciones.
### Funciones
```st
fn verificar(X) {
check valid X
return X
}
fn combinar(A, B) {
return A & B
}
verificar((P | !P))
let resultado = combinar(P, Q) | !R -- funciones como expresiones
```
### Proof blocks
```st
assume h1 : P -> Q
assume h2 : P
show Q
derive Q from {h1, h2}
qed
```
### Teorías (POO lógico)
```st
-- Singleton (sin parámetros)
theory Base {
axiom ley = P -> P
private let interno = Q
let publico = R
}
-- Con parámetros (instanciable como clase)
theory Agente(id, creencia) {
let nombre = id
axiom p = creencia
fn saludar() {
print nombre
}
}
let a1 = Agente("Socrates", P)
a1.saludar()
check valid a1.p
print Base.publico -- acceso con punto
```
Herencia:
```st
theory Extendida extends Base {
axiom otra = Q -> Q
}
```
### Módulos
```st
-- lib.st
export let Identidad = P -> P
export fn doble_neg(phi) { return !!phi }
let Interno = Q & !Q -- no se exporta
-- main.st
import "lib.st"
check valid Identidad
```
### Text Layer
```st
let p = passage([[documento.md#seccion-2]])
let f = formalize p as (P -> Q)
claim c1 = f
support c1 <- p
confidence c1 = 0.84
context c1 = "Lectura conservadora"
render claims
```
---
## Operadores
### Proposicional (precedencia de menor a mayor)
| Op | Significado |
|---|---|
| `<->` | Bicondicional |
| `->` | Implicación |
| `|` | Disyunción |
| `^` / `xor` | XOR |
| `!|` / `nor` | NOR |
| `&` | Conjunción |
| `!&` / `nand` | NAND |
| `!` | Negación |
### Primer orden
`forall x`, `exists x`, `P(x)`, `x = y`
### Modal / Deóntica / Epistémica
`[]` (necesario/obligatorio/conocido), `<>` (posible/permitido)
### Temporal
`next P`, `P until Q`
### Aritmética
`+`, `-`, `*`, `/`, `%`, `<`, `>`, `<=`, `>=`
---
## Alias en español
| Inglés | Español |
|---|---|
| `logic` | `logica` |
| `axiom` | `axioma` |
| `theorem` | `teorema` |
| `derive` | `derivar` |
| `from` | `desde` |
| `check valid` | `verificar valido` |
| `check satisfiable` | `verificar satisfacible` |
| `countermodel` | `contramodelo` |
| `truth_table` | `tabla_verdad` |
| `analyze` | `analizar` |
| `explain` | `explicar` |
| `import` | `importar` |
| `export` | `exportar` |
| `theory` | `teoria` |
| `private` | `privado` |
| `if` | `si` |
| `else` | `sino` |
| `for` | `para` |
| `while` | `mientras` |
| `fn` | `funcion` |
| `return` | `retornar` |
---
## API programática (TypeScript/JavaScript)
```typescript
import { evaluate, createInterpreter } from '@/lib/st-api';
// Stateless: corre un script completo de una vez
const result = evaluate(\`
logic classical.propositional
let regla = P -> Q
let hecho = P
derive Q from {regla, hecho}
\`);
console.log(result.results[0].status);
// Stateful: útil para REPLs y sesiones interactivas
const st = createInterpreter();
st.exec('logic arithmetic');
st.exec('explain 2 + 3 * 4');
```
---
## Secciones de DOCS.md (referencia rápida)
| Sección | Tema |
|---|---|
| §1 | Modelo mental de ST |
| §2 | Estructura mínima de un script |
| §3 | Statements principales |
| §4 | Variables, alias y scripting (`let`, `set`, `print`) |
| §5 | Control de flujo (`if`, `for`, `while`) |
| §6 | Funciones (`fn`, `return`) |
| §7 | Proof blocks (`assume`, `show`, `qed`) |
| §8 | Teorías, encapsulación y herencia (POO) |
| §9 | Módulos (`import`, `export`) |
| §10 | Text Layer |
| §11 | Perfiles lógicos soportados (11 perfiles) |
| §12 | Operadores y precedencia |
| §13 | Alias en español |
| §14 | CLI |
| §15 | API programática |
| §16 | Integración con editores (protocolo LSP) |
| §17 | Ejemplos recomendados |
| §18 | Buenas prácticas |
| §19 | Limitaciones y notas de precisión |
| §20 | Receta pedagógica sugerida |
---
## Notas de precisión
- `classical.propositional` es el perfil más completo y probado.
- `truth_table` y `check equivalent` dependen de que el perfil los implemente.
- `while` tiene límite de 1000 iteraciones para evitar loops infinitos.
- `return` dentro de `fn` corta la ejecución; las funciones también pueden usarse como expresiones en fórmulas.
- Las teorías sin parámetros actúan como singletons (se instancian al declararse).
- Solo `let`, `axiom`, `theorem`, `fn` y `theory` pueden ser `export`ados.
Pega este contenido al inicio de tu sesión con cualquier IA (Claude, ChatGPT, Gemini, Copilot…) para que comprenda el lenguaje ST sin necesidad de documentación adicional.