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.AI2011
Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries
Thierry Boy de la Tour, Mnacho Echenim
Symmetries occur naturally in CSP or SAT problems and are not very difficult to discover, but using them to prune the search space tends to be very challenging. Indeed, this usuall…