The Role of Horn Clauses in Automatic Reasoning

Christoph Weidenbach


The performance of automatic reasoning procedures relies on solving easy parts of a problem efficiently. For example, the CDCL calculus as well as SMT rely on partial models build from Horn clauses, actually literals. In the talk I discuss the role of Horn clause fragments in automatic reasoning for model building and simplification.