MPI-I-94-228

Symbolic reasoning in a logical framework becomes more and more important for computer applications such as Natural Language Processing Systems or Expert Systems. These applications usually need specifically tailored logics. Therefore we are developing methods and algorithms for supporting the designer of an application system, who is usually not a logician, to develop his own application oriented logic. This paper gives an overview about our current state of these investigations. In particular we consider the correspondences between axiomatic and semantic specifications of a logic and the problem of finding one from the other. Correlated with this area are translation methods from the object logic into predicate logic, and methods for optimizing the translation. Other topics are investigations of the expressiveness of a logic and the axiomatizability of semantic conditions. The basic techniques underlying our approach, so called K-transformations and quantifier elimination, are briefly discussed. They are quite general mechanisms for manipulating predicate logic formulae, and the investigation of logics is only one of their applications. For the technical details of the methods and the proofs I refer to the original papers.