Axiomatic constraint systems for proof search modulo theories

Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean Marc Notin

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


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.

Original languageEnglish
Title of host publicationFrontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Proceedings
EditorsCarsten Lutz, Silvio Ranise
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783319242453
Publication statusPublished - 1 Jan 2015
Externally publishedYes
Event10th International Symposium on Frontiers of Combining Systems, FroCoS 2015 - Wroclaw, Poland
Duration: 21 Sep 201524 Sep 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Symposium on Frontiers of Combining Systems, FroCoS 2015


Dive into the research topics of 'Axiomatic constraint systems for proof search modulo theories'. Together they form a unique fingerprint.

Cite this