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.
翻译:逻辑系统在问题解决方面的应用可能像数学中证明定理或是想方设法与朋友会面那样多种多样。在任何一种情况下,问题解决活动都可以通过寻找一个“论证”来捕捉,广泛地理解为一个解决问题的凭证。关键是,为了使这样一个凭证成为一个解决方案,它必须是“有效的”,而使它有效的就是根据底层逻辑系统推理的概念构建的。我们提供了一个一般的框架,统一描述了将逻辑系统作为推理数学所需的方式。我们使用杜梅特-普拉维茨传统中的证明论证明论,定义了论证的有效性,并使用战术证明理论来关联论证、推理和搜索。