# Theorem proving

Our goal is to develop techniques for proving formulas from expressive logics, which arise in domains such as software verification.

We are developing

- decision procedures for specialized theories
- techniques for combining different reasoning tools

### Decision procedures

We have developed decision procedures for following classes of constraints

- term powers: quantified combination of term algebras (i.e. theory of algebraic data types) and arbitrary decidable theories

### Combinating reasoning tools

One technique for combining reasoning tools that we found useful is described in Chapter 4 of Viktor Kuncak's dissertation.

### Application

We are applying our decision procedures in software verification, for example in the Jahob system.