Алгоритм упрощения логических выражений

Кто-нибудь знает алгоритм для упрощения логических выражений?

Я помню булеву алгебру и карты Карнаута, но это предназначено для цифрового оборудования, где ВСЕГДА является логическим. Я хотел бы что-то, что учитывает, что некоторые подвыражения не являются логическими.

Например:

a == 1 && a == 3

это может быть переведено в чистое логическое выражение:

a1 && a3 

но это выражение неприводимо, в то время как с небольшим знанием арифметики everibody может определить, что выражение является справедливым:

false

Кому-то известны ссылки?