Traditionally, a logic was a formal language with a precise semantics.
While computer science grew up a logic eventually evolved to a formal
language with a precise semantics, a proof theory, an actual implementation
and an application domain, designed to solve problems from the domain.
For example, some programming languages have a well-defined type concept
that can be used to automatically check well-typedness of a program at
compile time.
In my talk I will further motivate why it is important to study the automation of logics
in general, what have been main achievements in the last 20 years, what
are current challenges and speculate on what we will see in the future.