Name
Abstract | ||
|---|---|---|
We define 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., ∧i-1n pi, where n is a parameter). The satisfiability 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 specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1613/jair.3351 | Journal of Artificial Intelligence Research |
Keywords | DocType | Volume |
proof pattern,i-1n pi,satisfiability problem,particular class,large class,new logic,schemata calculus,undecidability result,propositional logic,propositional schema,general class,propositional formula schema | Journal | abs/1401.3900 |
Issue | ISSN | Citations |
1 | Journal Of Artificial Intelligence Research, Volume 40, pages
599-656, 2011 | 15 |
PageRank | References | Authors |
0.90 | 22 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Aravantinos | 1 | 86 | 10.29 |
| Ricardo Caferra | 2 | 303 | 29.85 |
| Nicolas Peltier | 3 | 50 | 11.84 |