2 papers
cs.AI2011
Instantiation Schemes for Nested Theories
Mnacho Echenim, Nicolas Peltier
This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures…
cs.LO2011
Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
This paper relates the well-known Linear Temporal Logic with the logic of propositional schemata introduced by the authors. We prove that LTL is equivalent to a class of schemata i…