Sciweavers

TABLEAUX
2009
Springer

A Schemata Calculus for Propositional Logic

14 years 7 days ago
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.
Vincent Aravantinos, Ricardo Caferra, Nicolas Pelt
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TABLEAUX
Authors Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
Comments (0)