Download lógica computacional ingeniería técnica - Mi portal

Jesús Cáceres Tello
Dpto. Ciencias de la Computación
LÓGICA COMPUTACIONAL
INGENIERÍA TÉCNICA INFORMÁTICA
Departamento de Ciencias de la Computación – Universidad de Alcalá
INTRODUCCIÓN
Objetivos y contenidos
El objetivo fundamental de esta asignatura es exponer los métodos de la lógica
(concretamente de la lógica de proposiciones y de la lógica modal) que más se utilizan hoy en
día en Ciencias de la Computación, Inteligencia Artificial e Ingeniería del Software.
Motivación para los alumnos de Ingeniería Informática
La lógica constituye la herramienta formal de razonamiento de la mayor parte de las
asignaturas de la carrera de informática, sobre todo de las que están más relacionadas con
las matemáticas y la programación, tales como Álgebra, Análisis Matemático, Matemática
Discreta, Electrónica Digital, Teoría de Autómatas y Lenguajes Formales, Programación (incluida
la Programación Concurrente y la Programación Declarativa), Bases de Datos, etc.…
-
En cuanto a la Inteligencia Artificial, la lógica es el fundamento de todos los métodos
de representación del conocimiento y del razonamiento, especialmente en sistemas
expertos, razonamiento con incertidumbre (encadenamiento de reglas, lógica difusa,
etc...), procesado del lenguaje natural, razonamiento espacial y temporal, visión
artificial, robótica, lógica epistémico, etc.…
-
En tercer lugar, los métodos formales tienen una aplicación inmediata en la Ingeniería
del Software. El uso de lenguajes de especificación formal es beneficioso en todos los
desarrollos, ya que promueve la definición de modelos estructurados, concisos y precisos
en diferentes niveles de abstracción, y facilita el razonamiento sobre ellos incluso a un
nivel informal. Cuando a las notaciones formales se les asigna una semántica operacional,
es posible diseñar herramientas automáticas que detecten ambigüedades en los
requisitos iniciales, verifiquen y validen modelos a lo largo del ciclo de desarrollo, ayuden
en la evolución y el mantenimiento de los productos y generen automática o semiautomáticamente prototipos o incluso partes del código final.
-
Finalmente los métodos formales sirven también para propósitos de documentación,
ingeniería inversa y reutilización de componentes. No obstante, aún siendo
reconocidas las importantes contribuciones de los métodos formales a la ingeniería del
software, su uso no se ha extendido tanto como cabía prever hace un par de décadas.
Lo cierto es que los proyectos de desarrollo formal han fracasado con frecuencia. La
experiencia ha mostrado que introducir métodos formales en un proceso de desarrollo
puede provocar dificultades no relacionadas con la potencia de los métodos.
1. En primer lugar, pueden resultar excesivamente restrictivos, tanto porque
obligan a sobre-especificar ciertos aspectos como porque constriñen el
proceso de desarrollo, que tienen tendencia a monopolizar.
2. En segundo lugar, su introducción puede ser problemática desde un punto de
vista práctico, debido a su dificultad real y percibida, de forma que el coste
inicial de entrenamiento en estas técnicas puede ser significativo, y en
1/4
Jesús Cáceres Tello
Dpto. Ciencias de la Computación
ocasiones los métodos son infrautilizados incluso por parte de ingenieros
instruidos en su uso.
Es un dicho conocido acerca de la lógica que dice “… es una técnica que siempre ha
tenido un gran éxito y siempre lo tendrá”.
El incremento en costes de desarrollo que los métodos formales suponen en las primeras
fases del ciclo software se puede ver no obstante compensado por el decremento de los costes
de las últimas fases, particularmente en la fase de validación, así como de las subsecuentes
fases de mantenimiento y evolución. Las dificultades antes referidas podrían solventarse si se
difundiesen pautas para seleccionar notaciones adecuadas para cada problema, evitar la sobreformalización, identificar dominios adecuados, integrar las técnicas formales con técnicas semiformales de uso extendido, comercializar herramientas de desarrollo amigables, desarrollar
técnicas específicas de estimación de costes de desarrollo, etc.…
En resumen, los avances realizados en la última década en este campo han hecho de los
métodos formales de verificación una herramienta cada vez más utilizada, y es de prever que su
uso se extienda significativamente en los próximos años. Las empresas más importantes del
mundo de la informática y las telecomunicaciones, como AT&T, BT, IBM, Intel, Motorota,
Siemens, SRI, etc.…, cuentan con equipos especializados en este tema y los profesionales que
conocen estas técnicas están cada vez más solicitados.
Entre las aplicaciones desarrolladas recientemente utilizando un proceso de desarrollo
enteramente formal cabe destacar la automatización de la nueva línea de metro de París,
METEOR, que ha obtenido una enorme publicidad. Esta línea funciona sin conductores y dejando
un pequeño margen temporal entre trenes, de modo que los requisitos de seguridad requieren
una alta confianza en el software.
Finalmente, aunque no se llegue a ser un experto en verificación, el estudio de la lógica
computacional puede aportar un beneficio importante: adquirir una mente lógica, que servirá
tanto para estudiar las asignaturas de la carrera como para, en la práctica profesional, poder
realizar con mayor éxito las labores de diseño y programación del software.
Historia
El primer paso hacia la inteligencia (artificial), desde el desarrollo de la lógica fue dado
por Aristóteles (384-322 a.C.), cuando empezó a explicar y a codificar ciertos estilos de
razonamiento deductivo que él mismo llamó silogismos.
En el siglo XIII, Ramón Llull, un místico y poeta catalán, construyó una máquina de
engranajes denominada “Ars Magna”, que supuestamente era capaz de responder a todo tipo de
preguntas. También “Ars Magna” fue el nombre de una obra en la que trató de exponer un
complicado método universal para probar las verdades de fe con un lenguaje abstracto que
prefigura la formalización lógica.
En 1673 Leibniz inventa la primera calculadora de propósito general llamada “Pascalina”.
Aunque el aparato podía ejecutar operaciones de multiplicación y división, padeció de problemas
de fiabilidad que disminuyeron su utilidad. Sin embargo, Leibniz concibió la idea de aplicar las
técnicas de la deducción matemática a los razonamientos filosóficos. El sistema se basaba en un
cilindro estriado. Cada estría es de una longitud distinta, dependiendo del número que
representa. Para realizar el movimiento de los cilindros existen unas ruedas dentadas móviles,
esta movilidad se usa para la asignación de valores, mediante unos botones para dicho fin. Una
vez indicado el valor, por medio de una manivela produciremos el movimiento necesario para
realizar la operación (suma o resta dependiendo del sentido del giro).
En 1769, el húngaro Wolfang Von Kempelen sorprendió al mundo entero con la invención
de una supuesta máquina pensante bautizada como “El Turco”, que poseía la habilidad de jugar
al ajedrez sin “aparente” intervención humana.
2/4
Jesús Cáceres Tello
Dpto. Ciencias de la Computación
(Anécdota): Se trataba de un dispositivo ingenioso, puramente mecánico, con la
apariencia de un turco. Este turco era más grande que una persona de tamaño natural. El
extraño muñeco estaba sentado ante una caja de 120 cm. De largo por 80 cm. De alto, en la
cual había colocado un tablero de ajedrez.
En el interior del cofre se encontraban una serie de finos engranajes, resortes
complicados y un cajón con las correspondientes piezas de ajedrez. El inventor “demostraba”
antes de cada partida, que su autómata no estaba trucado y abría las puertas de la gran caja
para demostrar que solamente contenía el mecanismo.
Levantaba también las ropas del muñeco para enseñar que dentro de él no había
nada sospechoso. El maniquí jugaba solo y ganaba las partidas más complicadas y difíciles que
se le presentaban.
Obviamente, la excepcional habilidad de su juego provenía de un maestro del
ajedrez escondido dentro de la máquina. Se trataba, por lo tanto, de un engaño.
Se supone que cualquier persona con dos dedos de frente que viera una caja
conteniendo sobre ella un tablero de ajedrez y un robot que juega como los dioses ganando a
cualquier competidor que se le ponga a tiro, tiene que deducir inevitablemente que es un truco,
inclusive los sofisticados ordenadores actuales que le pueden ganar a los mejores ajedrecistas
del mundo, como sucedió con “Deep Blue”, la máquina preparada por IBM, cuando compitió con
Kasparov tenía detrás de ella a los más expertos del mundo en ajedrez e informática.
Sin embargo, el robot construido por von Kempelen produjo encendidas polémicas
sobre su verdadero funcionamiento que hasta hoy persisten. Si alguien me invita a ver una vaca
que vuela, es obvio que me voy a reír, dando por sentado que están tomándome el pelo.
Sin embargo, a pesar de que la idea de un robot pensante que jugara
magistralmente al ajedrez tenía tanta verosimilitud como una vaca que volara, la gente, incluido
grandes personalidades y científicos de la época, concurrían asombrados a ver el prodigio.
El robot ajedrecista de von Kempelen no respetó ni al emperador José II ni a la zarina
Catalina II de Rusia. Ni siquiera Napoleón Bonaparte, con toda su astucia, consiguió descrubrir el
truco de esta máquina.
Es muy conocida la anécdota que se refiere a la supuesta primera derrota de Napoleón
en aquella exhibición que tuvo lugar en 1809, en el palacio vienés de Schönbrunn. Parece que la
máquina se atrevió a ganarle al poderoso emperador tres veces consecutivas. Después de su
tercera derrota, Napoleón perdió el dominio de sí, y con furia barrió todas las piezas del tablero
arrojándolas al suelo. Claro, Bonaparte no sabía que en realidad se había enfrentado al célebre
campeón austriaco de ajedrez Johann Allgaier, escondido dentro de la caja.
En el siglo XIX, el matemático e inventor Charles Babbage concibió una máquina que se
adelantó más de cien años a su época y se puede considerar como la antecesora de los
actuales ordenadores, cuya realización sólo sería posible en pleno siglo XX después de la
Segunda Guerra Mundial. En 1820 Babbage estudió la posibilidad de construir una máquina capaz
de calcular con exactitud.
Fueron dos matemáticos, Boole y Frege quienes en 1854 formularon y desarrollaron las
leyes de un álgebra del pensamiento o álgebra lógica, que presentan el mismo grado de rigor y
exactitud que las leyes del álgebra matemática.
Diversos matemáticos (Post, Wittgenstein, Herbrand, Robinson…) fueron avanzando en el
estudio de la lógica durante el siglo XX y permitieron que en 1950, A. Turíng escribiera “Mind”,
sobre la posibilidad de que las máquinas adquirieran inteligencia, nació la Inteligencia Artificial
(IA).
3/4
Jesús Cáceres Tello
Dpto. Ciencias de la Computación
Turing inventó una prueba, conocida como la Prueba de Turing, para determinar si una
máquina es o no inteligente. La prueba consiste en aislar a dos personas (o bien, hombremáquina) cada una en una habitación y formular preguntas. Si el interlocutor llega a creer que
en la otra sala hay una persona cuando en realidad existe una máquina contestando, entonces
se puede decir que esa máquina es inteligente.
Según otros autores, la Inteligencia Artificial nació en 1943 cuando McCulloch y Pitts
propusieron un modelo de neurona del cerebro humano y animal.
Sitios de Interés
www.afm.sbu.ac.uk
www.cs.indiana.edu/formal-methods-education/
4/4