Otomatik teorem kanıtlama
Otomatik teorem kanıtlama, teoremlerin bilgisayar programları aracılığıyla kanıtlanmasına odaklanan matematiksel mantık dalıdır. Otomatik yordamlar için matematiksel kanıt yönteminin kullanılması bilgisayar biliminin gelişiminde kilit rol oynamıştır.
Allen Newell, Herbert A. Simon ve J. C. Shaw tarafından geliştirilmiş Logic Theorist programı önerme mantığına ait kanıtlar sunmaktadır.
 | Bilgisayar bilimi ile ilgili bu madde taslak seviyesindedir. Madde içeriğini genişleterek Vikipedi'ye katkı sağlayabilirsiniz. |