2 citations · 5 across the 12 of their papers we have counts for
4 papers · 1 filter
Axiomatic constraint systems for proof search modulo theories
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand +2
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…
Sequent Calculi with procedure calls
Mahfuza Farooque, Stéphane Graham-Lengrand
In this paper, we introduce two focussed sequent calculi, LKp(T) and LK+(T), that are based on Miller-Liang's LKF system for polarised classical logic. The novelty is that those se…
Two simulations about DPLL(T)
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
In this paper we relate different formulations of the DPLL(T) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T). The second formulatio…
A sequent calculus with procedure calls
Mahfuza Farooque, Stéphane Lengrand
In this paper, we extend the sequent calculus LKF into a calculus LK(T), allowing calls to a decision procedure. We prove cut-elimination of LK(T).