Axiomatic constraint systems for proof search modulo theories

Abstract : Goal-directed proof search in first-order logic uses meta-variables 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 proof-search 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.
Type de document :
Communication dans un congrès
C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14>


https://hal.inria.fr/hal-01107944
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 21 janvier 2015 - 20:39:53
Dernière modification le : vendredi 17 février 2017 - 16:14:07

Identifiants

Citation

Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi. Axiomatic constraint systems for proof search modulo theories. C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14>. <hal-01107944>

Partager

Métriques

Consultations de la notice

268