The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an \emph{argument}, broadly conceived as a certificate for a solution to the problem. Crucially, for such a certificate to be a solution, it has be \emph{valid}, and what makes it valid is that they are well-constructed according to a notion of inference for the underlying logical system. We provide a general framework uniformly describing the use of logic as a mathematics of reasoning in the above sense. We use proof-theoretic validity in the Dummett-Prawitz tradition to define validity of arguments, and use the theory of tactical proof to relate arguments, inference, and search.

翻译：逻辑系统在问题求解中的应用可能多种多样，既可用于数学定理的证明，也可用于谋划如何与朋友会面。在这两种情形中，问题求解活动都体现为对广义上可视为问题解证书的"论据"的搜寻。至关重要的是，此类证书要成为有效解，必须满足"有效性"条件——其有效性源于根据底层逻辑系统的推理概念进行的恰当建构。我们提出了一个统一描述上述意义上逻辑作为推理数学的通用框架。采用达米特-普拉维茨传统的证明论有效性来定义论据的有效性，并运用策略式证明理论关联论据、推理与搜索过程。