Model Generation Automated Deduction: Efficient Algorithms for Selected Applications

The goal of automated deduction is to develop automatic or semi-automatic methods for proof search in formal logical systems in order to solve problems in mathematics, computer science or engineering disciplines. This project seeks to build on the expertise of the two collaborators to develop efficient automated deduction algorithms to solve the problems encountered in two important application domains, namely "circuit design, testing and diagnostics" and "data manipulation in deductive databases". The algorithms will be based on the powerful "model generation" paradigm which makes it possible to treat seemingly unrelated applications like the ones mentioned in a cross-fertilizing way.