TY - GEN
T1 - Axiomatic constraint systems for proof search modulo theories
AU - Rouhling, Damien
AU - Farooque, Mahfuza
AU - Graham-Lengrand, Stéphane
AU - Mahboubi, Assia
AU - Notin, Jean Marc
PY - 2015/1/1
Y1 - 2015/1/1
N2 - Goal-directed proof search in first-order logic uses metavariables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proofsearch procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.
AB - Goal-directed proof search in first-order logic uses metavariables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proofsearch procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.
UR - https://www.scopus.com/pages/publications/84950126779
UR - https://www.scopus.com/pages/publications/84950126779#tab=citedBy
U2 - 10.1007/978-3-319-24246-0_14
DO - 10.1007/978-3-319-24246-0_14
M3 - Conference contribution
AN - SCOPUS:84950126779
SN - 9783319242453
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 220
EP - 236
BT - Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Proceedings
A2 - Lutz, Carsten
A2 - Ranise, Silvio
PB - Springer Verlag
T2 - 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015
Y2 - 21 September 2015 through 24 September 2015
ER -