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

JAIR

2011

2011

We deﬁne a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions (e.g., pi) and iterated connectives ∨ or ∧ ranging over intervals parameterized by arithmetic variables (e.g., ∧n i=1 pi, where n is a parameter). The satisﬁability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus (called stab) allows one to capture proof patterns corresponding to a large class of problems speciﬁed in propositional logic. We also show that the satisﬁability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.

Related Content

Added |
14 May 2011 |

Updated |
14 May 2011 |

Type |
Journal |

Year |
2011 |

Where |
JAIR |

Authors |
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |

Comments (0)