В данной статье описывается программа, с помощью которой студент, изучающий метод резолюций, сможет рассмотреть его на примере любого множества логических формул любой интерпретации.