This thesis designs a theoretical and general framework where proof-search can modularly interact with domain-specific procedure(s). This framework is a focussed sequent calculus for polarised classical logic, with quantifiers, and it is designed in the view of capturing various computer-aided reasoning techniques that exist in logic programing, goal-directed systems, proof-assistants, and automated provers. This thesis starts with a survey of focused sequent calculi for polarised classical logic, as a journey from Gentzen's original sequent calculus to Liang-Miller's LKF. It then introduces a new system LKp(T) which extends, with on-the-fly polarisation and calls to decision procedures, Liang-Miller's LKF. Key results of the meta-theory of the system are proved: the cut-elimination property, the property that changing the polarity of connectives does not change the provability of formulae, and finally, the logical completeness of LKp(T). While Gentzen's original rules offer a lot of non-determinism in proof…