Abstract
It is well-known that safety verification can be captured in Constrained Horn Clauses (CHC). This is, however, not the case with liveness/termination, where people typically resort to ad-hoc extensions of CHC (e.g. with predicates that check whether a relation is well-founded). Here we propose a more general approach, namely the extension of CHC with so-called Ramsey quantifiers, which assert the existence of infinite cliques in the graph induced by some formula. We provide evidence for this to be the right extension by showing that Ramsey quantifiers can be effectively eliminated in common SMT theories (linear integer/real arithmetic), which can directly be applied to liveness verification for several infinite-state systems.