Komputa logiko
La komputa logiko estas la matematika logiko aplikita al la kunteksto de la komputoscienco. Ties uzo estas fundamenta en variaj niveloj: en la komputaj cirkvitoj, en la logika programaro kaj en la analizo kaj optimigo (de tempaj kaj spacaj rimedoj) de algoritmoj.
La logiko etendiĝas al la kerno de la informadiko dum ĝi aperas kiel fako: nome la verko de Alan Turing pri la Entscheidungsproblem (decidproblemo) sekve de la laboro de Kurt Gödel pri nekompletaj teoremoj. La nocio de la komputilo de ĝenerala uzado kiu aperis el tiu laboro estis ege grava por la desegnistoj de la informadika maŝinaro en la 1940-aj jaroj.
En la 1950-aj kaj 1960-aj jaroj, esploroj antaŭdiris, ke, kiam la homa sciaro povu esprimi sin uzante la logikon kun matematikaj notacioj, estus eble krei maŝinon kapablan rezoni nome artefarita intelekto. Tio rezultis pli malfacila ol esperita pro la komplekseco de la homa rezonado. En la logiko de programaro, programo konsistas en kolekto de aksiomoj kaj reguloj. La sistemoj de logika programaro (kiel Prolog) kalkulas la konsekvencojn de la aksiomoj kaj de la reguloj organizitaj por respondi konsulton.
Aktuale, la logiko estas etende aplikita en la kampoj de artefarita intelekto kaj de sciencoj de komputiko, kaj tiuj kampoj havigas riĉan fonton de problemoj en la formala kaj neformala logikoj. La teorio de la argumentado estas bona ekzemplo de kiel la logiko estas aplikata al la artefarita intelekto.