Reasoning on schemata of formulæ

DOI10.1007/978-3-642-31374-5_21MaRDI QIDQ2907331zbMATHOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier

Publication date 7 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1204.2990

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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.

Recommendations

• Schemata of SMT-problems
• Reasoning on schemas of formulas: an automata-based approach
• Complexity of the satisfiability problem for a class of propositional schemata
• A Schemata Calculus for Propositional Logic
• A decidable class of nested iterated schemata

Cited in

(6)

• Schemata of SMT-problems
• Schematic refutations of formula schemata
• Tractable and intractable classes of propositional schemata
• Reasoning on schemas of formulas: an automata-based approach
• scientific article; zbMATH DE number 1927428 (Why is no real title available?)
• Schemata of formulæ in the theory of arrays

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)