Studujeme dokazatelnost formulí v hilbertovských kalkulech pro neklasické výrokové logiky metodami automatického dokazování vět.