automatisk bevisföring
automatisk bevisföring, verksamheten att med en mer eller mindre allmän metod bevisa teorem inom en logisk eller matematisk teori med hjälp av datorer (vilket inte skall förväxlas med datorberäkningar som ett led i bevis av specifika matematiska teorem).
När en logisk eller matematisk teori formuleras som ett formellt system skapas en principiell möjlighet att med hjälp av en algoritmisk metod – dvs. genom ett på förhand helt bestämt, regelstyrt förfarande – bevisa vilket som helst teorem i teorin. Med tillkomsten av datorer blev det möjligt att använda sådana
Litteraturanvisning
Information om artikeln
Medverkande
Dag Prawitz
Källangivelse