2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2012)

Timisoara, Romania Romania

Sept. 26, 2012 to Sept. 29, 2012

ISBN: 978-1-4673-5026-6

pp: 111-118

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 MetTeL2, an automated tableau prover generator, to provide an implementation of the calculus and give experimental results using the prover.

INDEX TERMS

Automated Reasoning, Temporal Logic, Constraints, Tableau Calculus

CITATION

C. Dixon, B. Konev, R. A. Schmidt and D. Tishkovsky, "Labelled Tableaux for Temporal Logic with Cardinality Constraints,"

*2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing(SYNASC)*, Timisoara, Romania Romania, 2012, pp. 111-118.

doi:10.1109/SYNASC.2012.47

CITATIONS

SEARCH