Axiomatisation of constraint systems to specify a tableaux calculus modulo theories.
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin · arXiv (Cornell University) · 2014
Abstract In this paper we explore a proof-theoretic approach to the com-bination of generic proof-search and theory-specific procedures, in presence of quantifiers. Forming the basis of tableaux methods, the sequent calculus is re-fined with meta-variables (a.k.a existential variables or free variables) to delay the choice of witnesses, and parameterised by theory-specific features based on a system of constraints for meta-variables. An axiomatisation of these features is given, so that the soundness and completeness of the sequent calculus with meta-variables can be generically proved (with respect to the sequent calculus where the choice of witnesses is not delayed). We then describe a theory-generic proof-search implementation, that is parameterised by a theory-specific mod-ule whose specification is given by the above axiomatisation. 1