Decidability and Undecidability Results for Propositional Schemata

DOI10.1613/JAIR.3351zbMATH Open1220.68087arXiv1401.3900OpenAlexW2095943001WikidataQ129517862 ScholiaQ129517862MaRDI QIDQ2996912FDOQ2996912

Nicolas Peltier, Vincent Aravantinos, Ricardo Caferra

Publication date: 4 May 2011

Published in: Journal of Artificial Intelligence Research (Search for Journal in Brave)

Abstract: We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.

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

zbMATH Keywords

iterationstableau proofscoding of Post correspondence problempropositional formula schemata

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Logic in artificial intelligence (68T27) Decidability of theories and sets of sentences (03B25)

Cited In (5)

• A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata
• Reasoning on Schemas of Formulas: An Automata-Based Approach
• Schemata of SMT-Problems
• Schematic refutations of formula schemata
• Cut-Elimination and Proof Schemata

Uses Software

• Zinc
• SPIKE

This page was built for publication: Decidability and Undecidability Results for Propositional Schemata

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