Complexity of the Satisfiability Problem for a Class of Propositional Schemata

Abstract. 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. Vn i=1 andWn i=1 where n is a parameter. With these connectives the new logic includes formulae such as Vn i=1 (Pi Pi+1) (atoms are of the form P1, Pi+5, Pn, . . . ). The satisfiability problem for such a schema S is: "Are all the formulae denoted by S valid (or satisfiable)?" which is undecidable [1]. In this paper we focus on a specific class of schemata for which this problem is decidable: regular schemata. We define an automatabased procedure, called schaut, solving the satisfiability problem for such schemata. schaut has many advantages over procedures in [1, 2]: 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 r...

• Type: Conference
• Year: 2010
• Where: LATA
• Authors: Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
• Keywords: Automata Theory, LATA 2010