ES_46_RV6 - DEMUESTRA

ES_46_RV6NO CERTIFICADOLean: COMPILA; TRADUCCION PARCIALProlog: ARBOL INCOMPLETOAuditoría: REQUIERE_REVISION

DOCUMENTO 46 — REVISIÓN 6

Documento publicado para examen. La compilación y el árbol no certifican la verdad de sus afirmaciones.

PDF MD JSON ADEC Evaluación Lean Veredicto JSON Salida Lean Código Lean Evaluación Prolog Prolog JSON Salida Prolog Código Prolog Auditoría final Auditoría JSON Salida auditoría

Instalar y comprobar SWI-Prolog

Instala SWI-Prolog y comprueba que el ejecutable está disponible:

winget install SWI-Prolog.SWI-Prolog swipl --version

Descarga el código Prolog del proyecto y ejecútalo en su directorio:

swipl -q -s ES_46_RV6.pl

Una ejecución correcta muestra RESULTADO PROLOG: ARBOL COMPLETO, el objetivo alcanzable y la cadena de dependencias en sintaxis Prolog.

Lectura rápida de las reglas:

a :- b, c. significa: a es cierta si b Y c son ciertas. a :- (b ; c). significa: a es cierta si b O c es cierta. a :- b, c, !. significa: alcanzadas b y c, se acepta esa rama y no se prueban alternativas posteriores para a.

El símbolo ! es el corte. Si se escribe otra condición después del corte, por ejemplo a :- b, c, !, d., Prolog todavía debe demostrar d.

DEMUESTRA parte del objetivo final y comprueba dependencias, referencias a conjuntos definidos y fórmulas extraídas. El cierre del árbol no demuestra la verdad matemática de las fórmulas.

Antes de resolverlo, audita todo el grafo y rechaza ciclos, auto-dependencias, referencias inexistentes, nodos duplicados y nodos declarados sin hecho o regla. Los nodos válidos que no intervienen en el objetivo se muestran como aviso informativo.

Una repetición idéntica se informa como redundancia; las definiciones incompatibles se rechazan. Un dossier pendiente puede publicarse con estado NO CERTIFICADO, nunca como resultado final verificado.