The following paper has been accepted for publication in ACM Transactions on Computational Logic:
Extensible Proof Systems for Infinite-State Systems, by Rance Cleaveland (University of Maryland, College Park) and Jeroen Keiren