Raonament Automàtic i Demostració de Teoremes

Descripció (molt simplista) de l'àrea

• Raonament Deductiu: es tracta d'arribar a conseqüències lògiques a partir d'uns certs axiomes preestablerts. L'apariència dels sistemes a voltes els fa semblar diferentes, però els problemes i aplicacions de sistemes gramaticals, de reescritura, basats en resolució i d'altres són, en general, extrapolables entre sí.


• Raonament Inductiu: el procés és justament el contrari: a partir de casos particulars s'intenten construir teories o conceptes que els expliquen. La mateixa idea s'ha aplicat a programació en allò que s'ha denominat "inductive programming".

Amb l'objectiu de focalitzar-se i poder abordar la deducció automática d'una manera més concreta, des dels anys seixanta la major part dels esforços s'han dirigit cap a l'estudi de sistemes deductius formals, principalment la demostració automática de teoremes (ATP) (matemàtics o no) i sa "filla" la programació lógico-funcional.

No obstant, últimament s'ha esbrinat la idea d'utilitzar sistemes purament formals per a estudiar també el procés inductiu o d'aprenentatge sense la necessitat d'incorporar dades del món exterior. Aquesta idea era prou coneguda ja en teoria de sistemes e inclús en matemàtiques, que vingué a anomenar-se "experimental mathematics". És a dir, els sistemes deductius d'uns pocs axiomes poden produir tal informació que s'ha de recórrer a eines inductives per a estudiar-los, crear nous conceptes, simplificar-los, modificar-los, refinar-los, i en fi, transformar-los. Com ja vé sent habitual últimament, és en informática a on primer s'intenta l'aplicació o desenvolupament de nous esforços.

En realitat, l'objectiu de minimització i transformació de sistemes formals seguint certs criteris d'optimalitat (número de axiomes, eficiència, cost computacional de les deduccions, etc.) es remunta, una volta més, als grecs.

Els meus interessos fonamentals en aquesta àrea d'interés s'orienten cap a l'estudi general de sistemes formals, de les demostracions (el punt de vista deductiu) i la creació de conceptes (el punt de vista inductiu) i sobre tot la relació existent entre totes dos. Dos convenciments em motiven en aquesta l'ínea: (1) per a fer demostracions d'un cert calibre es fa imprescindible la introducció de conceptes o lemes addicionals i que açò constituix per si mateixa una ampliació o modificació del sistema formal original i (2) si la creació de conceptes no té estratègia alguna, finalment s'acabarà utilitzant la força bruta del computadors i si sí que en té s'acabaran descobrint poc a poc aquestes línies d'actuació.

Per a aquesta mampresa es veu necessari l'establiment de una sèrie de criteris per a avaluar els sistemes formals a fi de que es puga determinar si les transformacions o comparacions que es realitzen duguen a bon terme, si es pot trobar algun tipus de monotonia o si certs mètodes de deducci&o; o inducci&o; són més apropiats que d'altres. Per a tot açò pareix innegable la necessitat de fer-se servir de lògiques d'ordre superior.

De tots els meus temes d'interés aquest és el que dedique la major part del meu temps i esforços ja que conformen principalment la temàtica i els objectius de la meua tesi. Per a obtindre més informació sobre el meu doctorat en el Departament de Lògica i Filosofia de la Ciència, pots punxar ací. Per una visió ràpida de què ha sigut la deducció automàtica en els últims 30 anys, pots llegir "Perspectivas de la Demostración Automática de Teoremas"

URL's sobre Raonament Automàtic

Pàgines Genèriques o Relacionades: