Complexity of the Satisfiability Problem for a Class of Propositional Schemata

  • Vincent Aravantinos
  • Ricardo Caferra
  • Nicolas Peltier
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6031)


Iterated schemata allow to define infinite languages of propositional formulae through formulae patterns. Formally, schemata extend propositional logic with new (generalized) connectives like e.g. \(\bigwedge^{n}_{i=1}\) and \(\bigvee^{n}_{i=1}\) where n is a parameter. With these connectives the new logic includes formulae such as \(\bigwedge^{n}_{i=1} {(P_i \Rightarrow P_{i+1})}\) (atoms are of the form P 1, P i + 5, P n , ...). The satisfiability problem for such a schema S is: “Are all the formulae denoted by S valid (or satisfiable)?” which is undecidable [2]. In this paper we focus on a specific class of schemata for which this problem is decidable: regular schemata. We define an automata-based procedure, called schaut, solving the satisfiability problem for such schemata. schaut has many advantages over procedures in [2,1]: it is more intuitive, more concise, it allows to make use of classical results on finite automata and it is tuned for an efficient treatment of regular schemata. We show that the satisfiability problem for regular schemata is in 2-EXPTIME and that this bound is tight for our decision procedure.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aravantinos, V., Caferra, R., Peltier, N.: A DPLL Proof Procedure For Propositional Iterated Schemata. In: Proceedings of the 21st European Summer School in Logic, Language and Information (Worskhop Structures and Deduction) (2009)Google Scholar
  2. 2.
    Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus For Propositional Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 32–46. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Baelde, D.: On the Proof Theory of Regular Fixed Points. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 93–107. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  4. 4.
    Bradfield, J., Stirling, C.: Modal Mu-Calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, vol. 3, pp. 721–756. Elsevier Science Inc., New York (2007)CrossRefGoogle Scholar
  5. 5.
    Brotherston, J.: Cyclic Proofs for First-Order Logic with Inductive Definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Bundy, A.: The Automation of Proof by Mathematical Induction. In: [14], pp. 845–911Google Scholar
  7. 7.
    Cleaveland, R.: Tableau-based Model Checking in the Propositional Mu-calculus. Acta Inf. 27(9), 725–747 (1990)zbMATHMathSciNetGoogle Scholar
  8. 8.
    Comon, H.: Inductionless induction. In: [14], ch. 14Google Scholar
  9. 9.
    Fisher, M., Rabin, M.: Super Exponential Complexity of presburger’s Arithmetic. SIAM-AMS Proceedings 7, 27–41 (1974)Google Scholar
  10. 10.
    Goré, R.: Tableau Methods for Modal and Temporal Logics. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, ch. 6, pp. 297–396. Kluwer Academic Publishers, Dordrecht (1999)Google Scholar
  11. 11.
    Hetzl, S., Leitsch, A., Weller, D., Paleo, B.W.: Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM), July 2008, pp. 21–41 (2008)Google Scholar
  12. 12.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Pu. Co., Reading (1979)zbMATHGoogle Scholar
  13. 13.
    Immerman, N.: Relational Queries Computable in Polynomial Time (Extended Abstract). In: STOC ’82: Proceedings of the fourteenth annual ACM symposium on Theory of computing, pp. 147–152. ACM, New York (1982)CrossRefGoogle Scholar
  14. 14.
    Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2. Elsevier/MIT Press (2001)Google Scholar
  15. 15.
    Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-shaped Proofs in the mu-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 425–440. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Vincent Aravantinos
    • 1
  • Ricardo Caferra
    • 1
  • Nicolas Peltier
    • 1
  1. 1.Grenoble University (LIG/CNRS) 

Personalised recommendations