Unification Types in Logic

Unifikacja jest stosowana powszechnie w informatyce i w automatycznej dedukcji, w sztucznej inteligencji, a także w lingwistyce matematycznej (gramatyki kategorialne).

W pracy badane jest zagadnienie unifikacji w logikach: fregowskich i niefregowskich, modalnych i wielomodalnych, w tym w logikach czasowych (temporalnych) i logikach epistemicznych. Rozważa się warunki, w których unifikacja jest unitarna (tzn. najlepsza), jak np. przechodniość, sprzężoność, zbieżność, warunek Churcha–Rossera. Unifikacja ma zastosowanie ponadto w problemie dopuszczalności reguł dowodzenia.