A logic is presented for reasoning on iterated sequences of formulæ over some given base language. The considered sequences, or schemata, are defined inductively, on some algebraic structure (for instance the natural numbers, the lists, the trees etc.). A proof procedure is proposed to relate the satisfiability problem for schemata to that of finite disjunctions of base formulæ. It is shown that this procedure is sound, complete and terminating, hence the basic computational properties of the base language can be carried over to schemata. © 2012 Springer-Verlag.
CITATION STYLE
Echenim, M., & Peltier, N. (2012). Reasoning on schemata of formulæ. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7362 LNAI, pp. 310–325). https://doi.org/10.1007/978-3-642-31374-5_21
Mendeley helps you to discover research relevant for your work.