@INPROCEEDINGS{DixonKonevSchmidtTishkovsky12,
AUTHOR = {Dixon, C. and Konev, B. and Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2012},
TITLE = {Labelled Tableaux for Temporal Logic with Cardinality Constraints},
BOOKTITLE = {Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012)},
PUBLISHER = {IEEE Computer Society},
PAGES = {111--118},
ISBN = {978-1-4673-5026-6},
DOI = {http://doi.ieeecomputersociety.org/10.1109/SYNASC.2012.47},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/DixonKonevSchmidtTishkovsky12.html}},
ABSTRACT = {
Frequently when formalising systems that change over time, we must represent
statements, coming from physical constraints or representational issues,
stating that exactly $n$ literals (or less than~$n$ literals) of a set hold. 
While we can write temporal formulae to
represent this information, such formulae both complicate and increase
the size of the specification and adversely affect the performance of
provers. In this paper, we consider reasoning about problems specified
in propositional linear time temporal logics in the presence of such
constraints on literals. We present a sound, complete and terminating
tableau calculus which embeds constraints into its construction avoiding
their explicit evaluation. We use MetTeL, an automated tableau prover
generator, to provide an implementation of the calculus and give
experimental results using the prover.
}
}