Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LATA

2010

Springer

2010

Springer

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...

Related Content

Added |
02 Mar 2010 |

Updated |
02 Mar 2010 |

Type |
Conference |

Year |
2010 |

Where |
LATA |

Authors |
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |

Comments (0)