Hi, For what type systems / logics are there term / proof generation algorithms? What are their complexities? E. g. simply typed lambda-calculus / intuitionistic calculus... Milner type system... ... I will appreciate links to related papers. Thank you in advance, Lukasz