General logical formalisms
such as predicate logic, set theory, or number theory are undecidable
or even not recursively enumerable. However, such generality is not needed
in all applications: Important special cases such as the theory of integers
with addition are decidable, as well as the theory of lists or of arrays.
For computeraided reasoning, it is vital to combine general deductive
mechanisms like resolution with decision procedures for special structures
in order to succeed in the respective application areas. Substantially
more properties can then be proved automatically. Thus the practical applicability
of corresponding tools (e.g. for verification) is improved considerably.
In the seminar fundamental
methods for the construction of decision procedures have been discussed.
One may distinguish semantical methods, quasisemantical methods and prooftheoretical
ones; a further source is automata theory. Finally, the question has been
considered how and under which conditions such special procedures can
be combined and integrated into more general ones.
Three seminar sessions have
been held from December 01 until February 02. If you have further questions
regarding the seminar, please contact Thomas
Hillenbrand.
