2012 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2012)
Sept. 26, 2012 to Sept. 29, 2012
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.
calculus, inference mechanisms, temporal logic
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, 2013, pp. 111-118.