Breve presentación y lineas generales del proyecto.

Este proyecto consiste en implementar un demostrador automático para la lógica de primer orden. El objetivo principal es que el usuario escriba un conjunto de fórmulas como entrada al programa, y este decida si ese conjunto es o no inconsistene (existe o no un modelo que satisface todas las fórmulas del conjunto). Esto es equivalente a decidir si una fórmula en concreto es consecuencia lógica de un conjunto, es decir, se parte de una serie de premisas que se consideran ciertas y buscamos llegar a la conclusión deseada.

Existe ya hechos algunos demostradores parecidos, para mí, el más significativo es Otter (http://www-unix.mcs.anl.gov/AR/otter/). La idea es ofrecer una interfaz un poco más comoda que este, sin perder un apice de funcionalidad, además, se pretende hacer una implementación algo mas eficiente haciendo uso de multi-threads.

En posteriores post se desgranarán las fases de las que consta el proceso, se explicaran los algoritmos y se expondran los requisitos y el diseño del sistema, pero a grandes rasgos se podría decir que lo que hay que hacer es un parseador de la entrada, convirtiendo el texto introducido por el usuario en las estructuras de datos usadas por el programa (se hará uso de la herramienta antlr), hacer un tratamiento de las fórmulas introducidas (conversión a formas normales) y aplicar un algoritmos de resolución que nos lleve al resultado.

No esta cerrada la decisión de las herramientas y lenguajes a utilizar, pero posiblemente el proyecto será escrito en c#, con un compilador libre como shardevelop.

Es imposible resumir las posibles utilidades que tiene un sistema como este, por citar algunas, se pueden nombrar la verificación de sistemas, análisis y creación de circuitos lógicos o la web semántica (aunque parece que los demostradores que se usaran en un futuro en este campo trabajarán sobre otro tipo de lógica).

Hello world!

Welcome to WordPress.com. This is your first post. Edit or delete it and start blogging!