A Schemata Calculus for Propositional Logic

We define a notion of formula schema handling arithmetic parameters, indexed propositional variables (e.g. Pi) and iterated conjunctions/disjunctions (e.g. Vn i=1 Pi, where n is a parameter). Iterated conjunctions or disjunctions are part of their syntax. We define a sound and complete (w.r.t. satisfiability) tableaux-based proof procedure for this language. This schemata calculus (called stab) allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. Although the satisfiability problem is undecidable for unrestricted schemata, we identify a class of them for which stab always terminates. An example shows evidence that the approach is applicable to non-trivial practical problems. We give some precise technical hints to pursue the present work.

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
• Keywords: Artificial Intelligence, Propositional Variables, TABLEAUX 2009, Tableaux-based Proof Procedure, Vn I=1 Pi