Реализация солвера для логики первого порядка

Средства логики первого порядка в "зоне Златовласки" (Goldilocks Zone)
логического вывода достаточно выразительны, чтобы легко задать даже
сложные свойства, но при этом они достаточно просты для автоматизации.
На этой лекции мы обсудим реализации эффективных систем доказательства
теорем для логики первого порядка с равенством.

После короткого обсуждения логики и исчисления, будут обсуждаться
основные структуры современного солвера первого порядка, основанного на
"клозификации" (clausification) и насыщении (saturation) с устранением
избыточности. Если останется время, мы рассмотрим реализацию достаточно
подробно.

Особое внимание будет уделено поиску доказательств и важным (на
практике) техникам упрощения.