Entscheidungsverfahren für komplexe logische Theorien

The formal description of certain systems is composed of parts which originate from different areas. For example, in the description of a program, numerical formulas are found next to statements about data structures; the description is correspondingly more complicated

for complex systems with embedded software with access to different databases.

To model such systems, we use combinations of logical theories that formalize the individual parts in the description of the system.

The goal of this long-term project is to develop proof procedures for these kinds of complex logical theories that exploit the modular structure of the theories and allow specialized provers to be used for reasoning in the subtheories. Such modular methods are particularly flexible and efficient and applicable in many domains (such as mathematics, verification, or knowledge representation).

Our methods have been implemented in the theorem prover H-PILoT.