Teoremen frogapen automatiko

Teoremen frogapen automatikoa (ingelesez Authomathed theorem proving edo ATP) arrazonamendu automatikoaren azpialorra da eta programa informatikoen bidez teorema matematikoak frogatzeaz arduratzen da.

Definizioa

Teoremen frogapen automatikoaren teknikak bereziki baliagarriak dira geometria euklidearreko teoremak frogatzeko.

Orokorrean, prozedura honakoa da:

Frogatu behar dugun teorema era aljebraikoan jartzen dugu: hipotesia $P_{i}(x_{1},\ldots ,x_{n})=0,i=1,\ldots ,k$ eta tesia $Q(x_{1},\ldots ,x_{n})=0$ motako baldintza gisa adierazten dira.
Teorema egiazkoa izango da $Q\,$ badago $P_{1},\ldots ,P_{k}$ -k sortutako idealean (beste era batera esanda $P_{1},\ldots ,P_{k}$ -en ezeztapenak $Q\,$ -ren ezeztapena inplikatzen badu).
Polinomio bat ideal batekoa izatearen problema aljebra konputazionaleko problema klasikoa da; problema hau ebazteko ohiko teknika bat Gröbner-en oinarri egokia kalkulatzea da.

Frogapen metodo honen eragozpena konplexutasun informatiko handia duela da.

Teorema bat deduzitzearen problema

Azpi-logikaren arabera, teorema bat baliozkoa den edo ez erabakitzea, zeregin oso erraz izatetik ezinezko izatera alda daiteke. Logika proposizionalaren ohiko kasurako, problema ondorioztatu daiteke baina NP-osoa da, eta beraz pentsatzen da denbora esponentzialeko algoritmoak soilik existitzen direla frogaren zeregin orokorrerako. Predikatuaren lehen ordenaren kalkulurako, Gödel-en osotasunaren teoremak adierazten du teoremak zehazki logikoki baliozko diren ongi eratutako formulak direla beraz, teoremen identifikazioa errekurtsio bidez zenbakigarria da, hots, edozein baliozko teorema ezustean frogatua izan daiteke errekurtso mugagabeekin. Baliogabeko proposizioak, emandako teoriak eskatzen ez dituen formulak hain zuzen ere, ezin dira beti aintzatetsiak izan. Gainera, zenbaki arrunten teoria duen teoria formal trinko batek, frogatu ezin daiteken egiazko proposizio bat du, kasu honetan definitu gabeko puntu batean amaitzen da proposizioa frogatzen saiatzen den programa frogatzaile bat.

Kasu hauetan, posible da lehen ordenako frogatzaile batek ez amaitu ahal izatea frogapen bat bilatzen ari den bitartean. Muga teoriko hauez gain, teoremaren frogatzaile praktikoek problema zail asko ebatzi ditzakete logika hauekin.

Erlazionatutako problemak

Erlazionatutako problema bat, baina sinpleagoa, frogapenaren egiaztapena da, non teorema batek duen frogapen erreal baten balioa egiaztatzen den. Hau egin ahal izateko, frogapeneko pausu bakoitza programa batek egiaztatzeko modukoa izan behar da.

Frogatzaile interaktiboek, sistemari pistak emango dizkion gizaki baten laguntza behar dute. Automatizazio graduaren arabera, frogapenak probatzeko edo frogapen bateko zati garrantzitsuak automatikoki egiteko balio dute. Frogatzaile automatikoak zeregin askotarako erabiltzen dira, kasu batzuetan adibidez, makina guztiz automatikoek teorema interesgarri eta zail asko frogatzea lortu dute, horien artean matematikari askok saihestu dituzten teoremak. Lorpen hauek noizbehinkakoak dira ordea. Orokorrean lan zailek adimen handiko erabiltzaile bat eskatzen dute.

Batzuetan teorema bat frogatzearen eta beste teknika batzuk erabiltzearen artean bereizketa bat egiten da. Prozesu batek teorema bat frogatzen duela kontsideratzen da, frogapen tradizionala badu, axiomekin hasi eta inferentziako pausu berriak egiñez. Beste teknika bat modeloaren egiaztapena da eta indar basati baten bidezko zenbakikuntza baten baliokidea da egoera askotan. Inteligentzia asko ere behar du indar basatiaz gain. Existitzen diren teorema hibridoen frogatzaileek modeloaren frogantza erabiltzen dute inferentzia erregela bezela. Programa batzuk teorema konkretu bat frogatzeko izan ziren sortuak, non programak balio batekin amaitzen badu, teorema egiazkoa dela esan daiteken. Honen adibide bat, 4 koloreen teorema da. Eztabaida handia piztu zen, gizakiek frogatu ezin zuten teorema bat (kalkulu handiegiak) lehenengo aldiz programa batek frogatu baitzuen. Baita ere, lauko artzain-jokoan beti lehenengo jokalariak irabazten duela ere frogatu zen.

Erabilera industriala

Teoremen frogapen automatikoa gehienbat industria elektrikoak erabiltzen du, zirkuitu integratuen diseinu eta egiaztapenean. Pentiumen FDIV bug-az geroztik, mikroprozesagailuen koma higikorreko unitate sofistikatu eta korapilatsuak azterketa gehigarriaren pausuak erabiliz diseinatu dira. AMD, Intel eta beste hainbaten prozesagailu modernoetan teoremen frogapen automatikoa erabili izan da zatiketa eta beste eragiketa matematikoak egoki diseinatuak izan diren ala ez egiaztatzeko. Teoremak frogatzeko bideetako bat ebazpenaren printzipioa da, inferentzia erregela bat bezala funtzionatzen duena eta nagusiki erregela zaharrenean oinarritua dagoena (Modus Ponens). Metodo hau axioma multzo bat frogatzean datza hauen gezurtapenaren bitartez, eta batzuetan premisak erabiliz.

Lehen mailako teoremen frogapena

Lehen mailako teoremen frogapena, gehitutako gaiak (konstanteak, funtzioen izenak eta aldagai askeak) dituen kalkulu proposizionala da, indukzio matematikoa adieraztea ezinezkoa egiten duena. Beraz, ez da matematikako lehen mailako teoriarekin nahastu behar, kuantifikatzaileak kendu baitira. Hala ere, kuantifikatzaile unibertsalak emulatu daitezke aldagai libreak bezala berridatziz.

Lehen mailako teoremen frogapena teoremen frogapen automatikoaren alor helduenetakoa da. Logika nahiko adierazgarria da eta problema arbitrarioen adierazpena ahalbidetzen du, askotan era natural eta intuitiboan egiten dena. Bestalde, oraindik semi-erabakikorra da eta hainbat kalkulu oso eta zuzen garatu dira, sistema guztiz automatikoen sorrera ahalbidetu dutenak.

Maila handiagoko logikak eta logika modalak bezalako logika adierazgarriagoek lehen mailako logikako problema gehiago era egokian adieraztea ahalbidetzen dute, baina problemen frogatzaileak gutxiago garatuta daude logika mota honetarako.

Liburutegiak eta lehiaketak

Inplementatutako sistemen kalitatea hobetu da erreferentziako adibideak dituen liburutegi handi bat dagoelako (TPTP) eta baita CASKek antolatutako ATP Lehiaketarengatik, lehen mailako teoremak frogatzeaz arduratzen diren lehen mailako sistemen urteroko lehiaketa.

Sistema nabarmen batzuk hurrengoak dira (bakoitzak gutxienez behin irabazi du CASC txapelketako kategoria batean).

-E errendimendu altuko lehen mailako teoremen frogatzailea da, ekuazioen kalkulu purutik sortua. Nagusiki Municheko Teknika Unibertsitateak garatua.

-Otter, Argonne National Laboratory, hedapen handia lortu zuen lehen teorema frogatzailea. Lehenengo mailako ebazpenean dago oinarritua. Otter Prover9rekin izan da ordeztua, Mace4 antzekoa dena.

-SETHEO errendimendu altuko sistema bat da, helburuei orientatutako ezabapen metodoan oinarrituta. Hau ere Municheko Teknika Unibertsitateak garatua da. E eta SETHEO konbinaturik (beste sistema batzuekin batera) E-SETHEO sortu dute. Vampire Manchesterreko unibertsitateak eta Andrei Voronkovek garatua da. Teorema frogatzaileen munduko txapelketa (ATP CADE) irabazi zuen kategoria entzutetsuenean 8 urtez (1999, 2001-2007).

Erreferentziak

Ingelesezko eta gaztelaniazko Wikipediaren itzulpena.

Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press.
Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.
Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer-Verlag Texts and Monographs in Computer Science, 421 pp.
Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers (Available for free download).
Duffy, David A. (1991). Principles of Automated Theorem Proving. John Wiley & Sons.
Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd ed.). McGraw–Hill.
Alan Robinson and Andrei Voronkov (eds.), ed. (2001). Handbook of Automated Reasoning Volume I & II. Elsevier and MIT Press.
Fitting, Melvin (1996). First-Order Logic and Automated Theorem Proving (2nd ed.). Springer.

Kanpo estekak

Datuak: Q431667