Aravantinos, V.; Caferra, R.; Peltier, N. Decidability and undecidability results for propositional schemata. (English) Zbl 1220.68087 J. Artif. Intell. Res. (JAIR) 40, 599-656 (2011). The authors consider propositional schemata built from \(\top\), \(\bot\), a set of propositional letters indexed by arithmetic expressions, and inequalities between arithmetic expressions, with operators negation, disjunction, conjunction and so-called iterations, that is, generalised disjunctions and conjunctions of the form \(\bigvee_{i=a}^b\phi\) and \(\bigwedge_{i=a}^b\phi\), where \(a\) and \(b\) are again arithmetic expressions, built from 0, successor, subtraction, addition and variables meant to range over the integers. Moreover, inequalities are not allowed to occur in the range of iterations. An interpretation \(\mathcal I\) of a schema \(\phi\) is then naturally determined by an assignment of true or false to the propositional letters and an assignment of integers to the integer variables; for instance, if \(\mathcal I\) assigns 3 to \(n\) then the truth value of \(\bigwedge_{i=1}^{n-1}p_{i+1}\) in \(\mathcal I\) is the truth value of \(p_2\wedge p_3\) in \(\mathcal I\). A bound-linear schema \(\phi\) is subjected to two additional constraints: (i) that it contains at most one parameter, that is, an integer variable \(n\) that is not bound in \(\phi\) in the sense that \(\phi\) contains no expression of the form \(\bigvee_{n=a}^b\) or \(\bigwedge_{n=a}^b\); (ii) that the arithmetic expressions that occur in \(\phi\), either as indices of propositional letters or as bounds of the ranges of iterations, are of the form (equivalent to) \(\alpha n+\varepsilon i+\beta\) where \(\alpha,\beta\in\mathbb{Z}\), \(\varepsilon\in\{-1,0,1\}\) and \(i\) is a bound integer variable, with \(\varepsilon =0\) if that arithmetic expression is \(a\) in an expression of the form \(\bigvee_{n=a}^b\) or \(\bigwedge_{n=a}^b\). The expressiveness of bound-linear schemata is illustrated with the formalisation of various properties of digital circuits, in particular, being an \(n\)-adder.Then the apparently much more restricted class of regular schemata is introduced; these contain no nested occurrence of iterations; further (i) every atom that occurs in an iteration of the form \(\bigvee_{i=a}^b\phi\) or \(\bigwedge_{i=a}^b\phi\) is of the form \(p_{i+\gamma}\) for some \(\gamma\in\mathbb{Z}\); (ii) all iterations have the same bounds. The authors prove that every bound-linear schema can be transformed into a regular schema such that one is satisfiable iff the other is, thanks to an algorithm shown to be of exponential complexity. The long proof is preceded by a semi-formal presentation that pedagogically explains the key aspects of the algorithm. This result allows the authors to prove that decidability of bound-linear schemata is decidable, thanks to a tableau proof procedure called stab (for schemata tableaux) that uses in particular (i) two iteration rules, namely, a rule that allows one to split a branch at a node labeled with a schema of the form \(\bigwedge_{i=a}^b\phi\), one child being labeled with \(\{b\geq a,\bigwedge_{i=a}^{b-1}\phi\wedge\phi[b/i]\}\), the other child being labeled with \(b<a\), and a rule that allows one to extend a branch at a node labeled with a schema of the form \(\bigvee_{i=a}^b\phi\) with a node labeled with \(\{b\geq a,\bigvee_{i=a}^{b-1}\phi\vee\phi[b/i]\}\); (ii) a closure rule that derives \(\{p_a,\neg p_b,a\neq b\}\) from \(\{p_a,\neg p_b\}\); (iii) a loop detection rule. A couple of proofs of some properties of \(n\)-bit adders are provided as examples, before stab is shown to be sound and complete with respect to satisfiability of any (fully general) schema, followed by a proof of termination of stab with respect to regular schemata. A description of a freely available implementation of stab is given together with sample examples of uses, outputs, and experimental results. Finally, it is shown, using an encoding of the Post correspondence problem, that two natural slight relaxations on the definition of regular schemata yield two undecidable classes; the proof is long and again preceded by a good overview of the key ideas. This last pair of results allows the authors to conclude that the class of bound-linear schemata is a good compromise between expressivity and tractability. Reviewer: Éric Martin (Sydney) Cited in 1 ReviewCited in 5 Documents MSC: 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) 03B05 Classical propositional logic 03B25 Decidability of theories and sets of sentences 68T27 Logic in artificial intelligence Keywords:propositional formula schemata; iterations; tableau proofs; coding of Post correspondence problem Software:SPIKE; Zinc PDFBibTeX XMLCite \textit{V. Aravantinos} et al., J. Artif. Intell. Res. (JAIR) 40, 599--656 (2011; Zbl 1220.68087) Full Text: DOI arXiv