Formas Prenex, de Skolem y Teorema de Herbrand

18 de Noviembre de 2020, ha tenido 26 vistas

Al igual que vimos cómo extender los Tableros Semánticos de LP a LPO, en este capítulo vamos a ver los fundamentos necesarios para extender las Formas Normales y Formas Clausales vistas en LP a un formato igualmente útil en LPO. El objetivo no solo es disponer de fórmulas equivalentes, sino ver hasta qué punto podemos trasladar los algoritmos que se desarrollan para LP al contexto de Primer Orden.

Etiquetas utilizadas: ,

Leer mas »

Formas Normales, Cláusulas y Algoritmo DPLL

10 de Noviembre de 2020, ha tenido 41 vistas

En este tema vamos a abordar los métodos más comunes de preprocesamiento de fórmulas LP, que también serán aplicables a fórmulas LPO, y mostraremos uno de los algoritmos centrales para $SAT$ que hace uso de este preprocesamiento, $DPLL$, en el que se basan la gran mayoría de métodos actuales que abordan ese problema.

Etiquetas utilizadas: ,

Leer mas »

Construir un buscador desde cero

3 de Noviembre de 2020, ha tenido 75 vistas

En esta entrada vemos cómo se pueden implementar de forma muy sencilla buscadores en Espacios de Estados en un lenguaje con características funcionales. La idea no es presentar implementaciones muy eficientes, sino únicamente encontrar patrones comunes y flexibles que permiten estas representaciones y posibles ampliaciones y adaptaciones futuras.

Etiquetas utilizadas: , , , ,

Leer mas »

Tableros Semánticos en Lógica de Primer Orden

28 de Octubre de 2020, ha tenido 42 vistas

Igual que la Lógica de Primer Orden extiende la Lógica Proposicional, el método de Tableros Semánticos que veremos para Lógica de Primer Orden se obtendrá añadiendo al método de la Lógica Proposicional mecanismos para manipular los nuevos operadores de construcción... pero habrá que tener cuidado con las peculiaridades de su mayor capacidad expresiva, lo que nos llevará a obtener un método que, como es de esperar, no es 100% automatizable, a pesar de ser muy útil e informativo.

Etiquetas utilizadas: , ,

Leer mas »

Tableros Semánticos en Lógica Proposicional

25 de Octubre de 2020, ha tenido 93 vistas

El método de los Tableros Semánticos proporciona un algoritmo para la decisión de la satisfactibilidad de un conjunto de fórmulas sin necesidad de preprocesamiento de las fórmulas. Su forma de operar consiste en ir simplificando los conjuntos de fórmulas por medio de operaciones que mantienen la consistencia hasta llegar a conjuntos de literales (fórmulas que, esencialmente son variables proposicionales) cuya consistencia podemos decidir con facilidad. Además de proporcionar un mecanismo muy potente de decisión, veremos que, si el conjunto es consistente, el método informa acerca de los posibles modelos que tiene.

Etiquetas utilizadas: , ,

Leer mas »

ALGUNAS ENTRADAS ANTERIORES ... AL AZAR

Teoría Algorítmica de la Información

28 de Marzo de 2012, 464 vistas

La Teoría Algorítmica de la Información (AIT) es el resultado de poner la Teoría de la Información de Shannon y la Teoría de la Computabilidad de Turing en una coctelera y agitar vigorosamente. La idea básica consiste en medir la complejidad de un objeto por el tamaño en bits del menor programa que lo calcula.

(Extraído del Prefacio escrito por G. Chaitin para la segunda edición del libro "Information and Randomness: An Algorithmic Perspective" de C. Calude)

Etiquetas utilizadas: , , , , ,

Sintaxis y Semántica de la Lógica de Primer Orden

17 de Octubre de 2020, 140 vistas

Aunque la Lógica Proposicional posee un semántica sencilla y existen algoritmos de decisión (aunque no sean eficientes) para los problemas básicos que hemos encontrado (SATTAUT y Problema de la consecuencia), su expresividad es bastante limitada, lo que hace que muchas situaciones no sean modelables en LP, bien porque requieren de mucho espacio (un gran número de fórmulas, y/o fórmulas de gran tamaño), o bien porque ni siquiera pueden expresarse en este lenguaje. Una Lógica de Primer Orden, también llamada lógica de predicados, es un sistema formal diseñado para estudiar la inferencia en los lenguajes de primer orden, que son lenguajes formales que extienden la Lógica Proposicional por medio de cuantificadores y símbolos que permiten hablar de los objetos de un dominio con predicados y funciones.

Etiquetas utilizadas: ,