Mantıksal bir dilde gösterilen bilgi üzerinde akıl yürütmek için kullanılan biçimsel ilkeler, ve algoritmalar (örn., SAT/QBF çözücüleri ve teorem ispatlayıcılar tarafından kullanılan yöntemler, ve bilgi derleme, mantıksal gerektirme, ve model sayma için kullanılan algoritmalar) ve bilgisayar bilimindeki uygulamaları (örn., geleceği teşhis ve test etme, planlama, model kontrolü, otomatik teorem ispatlama, kısıt sağlama).