Diskutují se uni- a multi-sukcedentové kalkuly pro intuicionistickou výrokovou logiku a zkoumá se složitost rozhodovacích procedur založených na těchto kalkulech.