În informatică, în special în reprezentarea cunoștințelor și raționamentul și metalogică, zona raționamentului automatizat este dedicată înțelegerii diferitelor aspecte ale raționamentului. Studiul raționamentului automatizat ajută la producerea de programe de calculator care permit computerelor să raționeze complet sau aproape automat. Deși raționamentul automatizat este considerat un subdomeniu al inteligenței artificiale, are și legături cu informatica și filosofia teoretică.
Cele mai dezvoltate subdomenii ale raționamentului automatizat sunt demonstrarea automată a teoremelor (și subdomeniul mai puțin automatizat, dar mai pragmatic al demonstrării teoremelor interactive) și verificarea automată a dovezilor (privită ca raționament corect garantat sub ipoteze fixe).De asemenea, s-a desfășurat o activitate extinsă în raționamentul prin analogie folosind inducția și abducția.[1]
Alte subiecte importante includ raționamentul sub incertitudine și raționamentul nemonoton.O parte importantă a domeniului incertitudinii este cea a argumentării, în care constrângeri suplimentare de minimalitate și consistență sunt aplicate pe lângă deducția automată mai standard. Sistemul OSCAR al lui John Pollock[2] este un exemplu de sistem automat de argumentare care este mai specific decât doar un demonstrator automat de teoreme.
Instrumentele și tehnicile de raționament automatizat includ logica și calculul clasic, logica fuzzy, inferența bayesiană, raționamentul cu entropie maximă și multe tehnici ad-hoc mai puțin formale.
Primii ani
Dezvoltarea logicii formale a jucat un rol important în domeniul raționamentului automatizat, care a dus în sine la dezvoltarea inteligenței artificiale.O dovadă formală este o dovadă în care fiecare inferență logică a fost verificată înapoi la axiomele fundamentale ale matematicii. Toate etapele logici intermediare sunt furnizate, fără excepție. Nu se face apel la intuiție, chiar dacă traducerea din intuiție în logică este de rutină. Astfel, o dovadă formală este mai puțin intuitivă și mai puțin susceptibilă la erori logice.[3]
Unii consideră că meeting-ul de la Cornell Summer din 1957, care a reunit mulți logicieni și informaticieni, este originea raționamentului automatizat sau a deducției automatizate [4] Alții spun că el a început mai înainte, cu programul Logic Theorist din 1955 al lui Newell, Shaw și Simon, sau cu implementarea de către Martin Davis în 1954 a procedurii de decizie a lui Presburger (care a demonstrat că suma a două numere pare este pară).[5]
Raționamentul automatizat, deși un domeniu semnificativ și popular de cercetare, a trecut printr-o „iarnă a inteligenței artificiale” în anii 80 și începutul anilor 90. Domeniul s-a reînviat ulterior. De exemplu, în 2005, Microsoft a început să folosească tehnologia de verificare în multe dintre proiectele sale interne și intenționează să includă o specificație logică și un limbaj de verificare în versiunea lor din 2012 a lui Visual C.[4]
Referințe
- Defourneaux, Gilles, and Nicolas Peltier. „Analogy and abduction in automated deduction.” IJCAI (1). 1997.
- John L. Pollock
- C. Hales, Thomas „Formal Proof”, University of Pittsburgh. Retrieved on 2010-10-19
- „Automated Deduction (AD)”, [The Nature of PRL Project]. Retrieved on 2010-10-19
- Martin Davis (1983). „The Prehistory and Early History of Automated Deduction”. In Jörg Siekmann; G. Wrightson (eds.). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. pp. 1–28. ISBN 978-3-642-81954-4. Aici: p.15
(Include texte traduse și adaptate din Wikipedia de Nicolae Sfetcu)
Introducere în inteligența artificială
Inteligența artificială s-a dezvoltat exploziv în ultimii ani, facilitând luarea deciziilor inteligente și automate în cadrul scenariilor de implementare. Inteligența artificială se referă la un ecosistem de modele și tehnologii pentru percepție, raționament, interacțiune și învățare. Asistăm la o convergență … Citeşte mai mult
Lasă un răspuns