Sciweavers

LATA
2010
Springer

Complexity of the Satisfiability Problem for a Class of Propositional Schemata

14 years 1 months ago
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...
Vincent Aravantinos, Ricardo Caferra, Nicolas Pelt
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where LATA
Authors Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Comments (0)