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.
Formas Prenex, de Skolem y Teorema de Herbrand
Formas Normales, Cláusulas y Algoritmo DPLL
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.
Construir un buscador desde cero
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.
Tableros Semánticos en Lógica de Primer Orden
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.
Tableros Semánticos en Lógica Proposicional
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.
- « Página anterior
- 1
- 2
- 3
- 4
- …
- 30
- Página siguiente »
ALGUNAS ENTRADAS ANTERIORES ... AL AZAR
Algoritmos de Clustering
Un algoritmo de clustering tiene como objetivo agrupar los objetos de un dataset según su similaridad, de forma que los objetos que hay dentro de un grupo (cluster) sean más similares que aquellos que caen en grupos distintos. Para resolver este problema se han desarrollado muchos algoritmos que se diferencian entre sí según qué se entiende por cluster (que, en esencia, viene dado por cómo definimos que dos objetos son más o menos similares) y por la eficiencia computacional a la hora de conseguir la agrupación final. En esta entrada haremos un recorrido por los más habituales de estos algoritmos.
De la Resolución Proposicional a la Resolución LPO
En esta entrada se presentan mecanismos para extender la Resolución Proposicional al contexto de los Lenguajes de Primer Orden. Esta entrada no es autocontenida, sino que está orientada a aclarar algunos conceptos de resolución en primer orden a los alumnos del curso de Lógica Informática, por lo que se supone que el lector ha asistido a las clases de esa materia y conoce la nomenclatura usada y los conceptos previos de los que depende.
