Reasoning on Schemata of Formulæ
From MaRDI portal
Publication:2907331
DOI10.1007/978-3-642-31374-5_21zbMATH Open1360.68746arXiv1204.2990OpenAlexW8401427MaRDI QIDQ2907331FDOQ2907331
Nicolas Peltier, Mnacho Echenim
Publication date: 7 September 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: A logic is presented for reasoning on iterated sequences of formulae 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 formulae. 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.
Full work available at URL: https://arxiv.org/abs/1204.2990
Cited In (2)
This page was built for publication: Reasoning on Schemata of Formulæ
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907331)
