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 use is typically through proof-search. A general framework supporting proof-search and its mechanization is the theory of tactics and tacticals; indeed, tactics provide both a uniform theory within which proof-search can be studied and a practical technology underpinning automated reasoning tools such as proof assistants. What is the semantics of a tactical system? What justifies tactical proofs as logical arguments? Proof-theoretic semantics is an approach to meaning centered exclusively on inference and proof. In this paper, we use proof-theoretic validity in the Dummett-Prawitz tradition to give a semantics for the theory of tactical proof in its full generality. This semantics is justified by showing that it arises naturally from the established relationship between tactics and logic, as well as being implicit in much of the literature on proof theory.
翻译:用于解决问题的逻辑系统的使用可能与在数学中证明理论理论或如何与朋友见面时一样多种多样。 在这两种情况下,使用通常都是通过证据搜索。支持证据搜索及其机械化的一般框架是战术和战术理论;事实上,战术提供了一种统一的理论,可以在其中研究证据研究,而一种支持自动推理工具(例如证据助理)的实用技术。战术系统的语义是什么?什么是战术系统的语义?什么是逻辑论点?证据理论语义是完全以推断和证据为中心的含义的一种方法。在本文中,我们使用Dummett-Prawitz传统中的校对理论有效性来为战术证据理论的完全概括性提供一种语义。这种语义学是有道理的,因为它自然产生于战术和逻辑之间的既定关系,并且隐含在大量证据理论文献中。