A decidable class of nested iterated schemata

DOI10.1007/978-3-642-14203-1_25MaRDI QIDQ5747768zbMATH OpenOpenAlexFDO

Authors Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_25

Mathematics Subject Classification ID

Classical propositional logic (03B05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Complexity of the satisfiability problem for a class of propositional schemata
• Decidability and undecidability results for propositional schemata
• Schemata of formulæ in the theory of arrays
• A Schemata Calculus for Propositional Logic
• Schemata of SMT-problems

Cites work

• A decidable class of nested iterated schemata
• A machine program for theorem-proving
• A Schemata Calculus for Propositional Logic
• Finite-model theory -- A personal perspective
• Handbook of automated reasoning. In 2 vols
• scientific article; zbMATH DE number 1614706 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• Inductionless induction
• Proof schemata in Hilbert-type axiomatic theories
• Schemata: The Concept of Schema in the History of Logic
• The automation of proof by mathematical induction

Cited in

(10)

• Reasoning on schemata of formulæ
• Decidability and undecidability results for propositional schemata
• Schemata of SMT-problems
• Complexity of the satisfiability problem for a class of propositional schemata
• On deciding satisfiability by theorem proving with speculative inferences
• A tableaux-based decision procedure for multi-parameter propositional schemata
• Tractable and intractable classes of propositional schemata
• A decidable class of nested iterated schemata
• RegSTAB: A SAT Solver for Propositional Schemata
• Metalinear recursive schemas on marked trees

This page was built for publication: A decidable class of nested iterated schemata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747768)