A coalgebraic framework for reductive logic and proof-search (ReLiC)

传统的逻辑演绎方法从推理开始，并以逐步的方式应用证明规则来推导结论，而补充的还原方法则从假定的结论开始，通过系统地减少可能的证明空间来搜索足以使合法推导存在的推理。这幅图不仅更接近于数学家实际证明定理的方式，更普遍地说，人们使用形式表示解决问题的方式，它还封装了逻辑在计算机科学中的各种应用，例如称为逻辑编程的编程范式，人工智能和自动定理证明的核心证明搜索问题，程序验证中的前提条件生成等等。它也反映在真值功能语义学的水平上--用于模型检查目的的逻辑的观点，从而验证工业系统的正确性--其中公式的真值是根据其组成部分的真值计算的。尽管还原观点反映了逻辑的实际应用，并与演绎逻辑形成鲜明对比，但还原逻辑并不存在统一的数学基础。皮姆、里特和瓦伦的工作提供了大量的背景，但这基本上限于经典和直觉主义逻辑，即使这样，也缺乏有关计算过程的明确理论。我们相信余代数-一个统一的数学框架计算，基于状态的系统和分解，其中席尔瓦是一个主要的贡献者和指数-可以应用于这一目的。演绎基本上是通过归纳结构来实现的，而归约则是通过共归纳的共代数技术来实现的，该技术将目标分解为子目标。已有的工作表明，余代数推广了真值函数语义，可以表示搜索空间的基本方面。我们将系统化这项工作的逻辑在充分的一般性，并通过利用coalgebraic的方法来建模的计算，也捕捉所需的控制程序的证明搜索。余代数的代数属性应确保该建模的所有方面，包括逻辑的定义，它们的搜索空间，和它们的搜索程序，将compositional.Beyond这一进步的最先进的语义方法证明搜索，我们可以希望利用计算的余代数表示，以实现更多。通过将证明搜索的共代数模型与例如概率计算或编程语言的共代数模型相连接，我们可以希望给出一个干净的，还原逻辑观点的应用的通用和模块化呈现，如归纳逻辑编程和溯因-将这些系统的关键特征抽象到一个模块化的语义框架中，可以帮助我们实现更多的功能。而不是简单地了解现有工具的工作原理并加以改进。这种框架还可以指导新工具的设计和实施。因此，在与我们的理论发展，我们将开发有效的，语义驱动的自动推理支持与广泛的应用。通过这样做，我们希望实现能够部署大范围推理问题的工具，并指导特定逻辑的定理证明器的设计。

While the traditional, deductive approach to logic begins with premisses and in step-by-step fashion applies proof rules to derive conclusions, the complementary reductive approach instead begins with a putative conclusion and searches for premisses sufficient for a legitimate derivation to exist by systematically reducing the space of possible proofs. Not only does this picture more closely resemble the way in which mathematicians actually prove theorems and, more generally, the way in which people solve problems using formal representations, it also encapsulates diverse applications of logic in computer science such as the programming paradigm known as logic programming, the proof-search problem at the heart of AI and automated theorem proving, precondition generation in program verification and more. It is also reflected at the level of truth-functional semantics --- the perspective on logic utilized for the purpose of model checking and thus verifying the correctness of industrial systems --- wherein the truth value of a formula is calculated according to the truth values of its constituent parts. Despite the reductive viewpoint reflecting logic as it is actually used, and in stark contrast to deductive logic, a uniform mathematical foundation for reductive logic does not exist. Substantial background is provided by the work of Pym, Ritter, and Wallen, but this is essentially restricted to classical and intuitionistic logic and, even then, lacks an explicit theory of the computational processes involved. We believe coalgebra --- a unifying mathematical framework for computation, state-based systems and decomposition, for which Silva is a leading contributor and exponent --- can be applied to this end. Deduction is essentially captured by inductive constructions, but reduction is captured through the coalgebraic technique of coinduction, which decomposes goals down into subgoals. Existing work shows that coalgebra generalizes truth-functional semantics and can represent basic aspects of search spaces. We will systematize this work to logics in full generality and, by utilizing the coalgebraic approach to the modelling of computation, also capture the control procedures required for proof-search. The algebraic properties of coalgebra should ensure that all aspects of this modelling, including the definitions of logics, their search spaces, and their search procedures, will be compositional.Beyond this advance on the state of the art in semantic approaches to proof-search,we can hope to utilize coalgebraic presentations of computation to achieve much more. By interfacing coalgebraic models of proof-search with coalgebraic models of, for example, probabalistic computation or programming languages, we can hope to give a clean, generic and modular presentation of applications of the reductive logic viewpoint as diverse as inductive logic programming and abduction-based Separation Logic tools such as Facebook's Infer.Abstracting the key features of such systems into a modular semantic framework can help with more than simply understanding how existing tools work and can be improved. Such a framework can also guide the design and implementation of new tools. Thus, in tandem with our theoretical development, we will develop efficient, semantically driven automated reasoning support with wide application. In doing so we can thus hope to implement tools capable of deployment for a large range of reasoning problems and guide the design of theorem provers for specific logics.