Automated Prover Generation

从程序验证、语义网的本体推理、多智能体系统到人工智能和文本挖掘，以及包括数学、计算语言学和哲学在内的许多计算领域都需要推理。成功的自动定理证明器可以确保在复杂的数学证明中获得更高的信任度，它们可以使我们能够自动消除软件系统和通信协议中的大类错误，并且它们可以用于支持大型知识库和基于Web的知识库的创建和推理。目前，需要应用程序自动推理工具的研究人员可以从头开始开发证明器;他们可以扩展和调整现有的证明器;他们可以将现有的证明器用于更广泛的逻辑，其中可以嵌入他们的逻辑，例如，一阶逻辑或高阶逻辑的证明器;或者他们可以使用逻辑框架或证明器开发平台。虽然这些方法已经取得了令人印象深刻的成功，所有这些方法都很难采用的用户没有显着的专业知识，在逻辑和自动推理。作为替代的目的，这个项目是自动生成实现证明。这个想法是，用户将能够定义他们的应用程序的逻辑形式化。这首先会自动转换为演绎演算，然后转换为实现的证明器。其工作方式类似于编译器或解释器，它自动将用高级编程语言编写的程序转换为机器码或字节码。不同之处在于，证明器生成器的输入不是一组指令，而是逻辑或理论的高级规范。该项目将侧重于自动生成tableau prover。Tableau证明器生成的基础将是我们在最近的工作中开发的Tableau演算合成框架，并且已经应用于许多逻辑。基于这个框架，所开发的软件将能够为给定的逻辑或理论自动生成一个健全的和完整的表演算。我们相信，现在有可能更进一步，开发软件，将自动生成一个实现自动定理证明这种演算。这将使非专家用户和开发人员能够以受支持的方式相对轻松地获得实现的证明器。对于用户至关重要的是，这消除了负担，关心证明的合理性，完整性和可判定性的结果，并实施或适应prover.We将扩展的理论基础的框架，以各种方式，以使其更加全面，并扩大范围的tableau方法的决策程序。将开发一系列工具：一个tableau prover生成器程序和辅助软件，以确保生成器和生成的prover的可靠性、正确性和效率。为了快速使用该技术并获得用户的反馈，第一个原型将在一年内完成并发布，并将组织两个教程。将对原型进行若干案例研究，以确定原型中可能需要修改和改进的重要问题。找到优化的关键领域是规则细化、证明器效率和框架的泛化。为了量化该项目的成功，开发的工具和生成的证明器的效用，用户的接受度和生成的证明器的实际效益的评估将进行。总体而言，自动化证明器生成是一个新的和困难的研究问题，但我们相信，它是一个真实的可能性，我们打算在这个项目中实现。

Reasoning is needed in many areas of computing from verification of programs, ontology reasoning for the semantic web, multi-agent systems to artificial intelligence and text mining and also other fields including mathematics, computational linguistics and philosophy. Successful automated theorem provers can ensure a much higher level of trust in complex mathematical proofs, they can enable us to automatically eliminate large classes of errors from software systems, and communication protocols, and they can be used to support the creation of and reasoning in large knowledge bases and web-based repositories.Implementing a fully-automated reasoning tool is a time-consuming and difficult undertaking. Currently, researchers requiring an automated reasoning tool for an application can develop a prover from scratch; they can extend and adapt an existing prover; they can use an existing prover for a wider logic into which their logic can be embedded, e.g., a prover for first-order logic or higher-order logic; or they can use logical frameworks or prover development platforms. While these approaches have led to impressive successes, all these approaches are difficult to adopt for users without significant expertise in logic and automated reasoning.As an alternative the aim of this project is to automatically generate implemented provers. The idea is that users will be able to define a logical formalisation of their application. This is automatically transformed first into a deduction calculus and then into an implemented prover. The way this is envisaged to work is similar to a compiler or interpreter, which automatically transforms a program written in a high-level programming language into machine-code or byte-code. The difference is that the input to the prover generator is not a set of instructions, but a high-level specification of a logic or a theory. This project will focus on the automated generation of tableau provers. The foundation for tableau prover generation will be a tableau calculus synthesis framework that we developed in recent work and have already applied to a number of logics. Based on this framework the software to be developed will be able to automatically generate a sound and complete tableau calculus for the given logic or theory. We believe that it is now possible to go further and develop software that will automatically generate an implemented automated theorem prover for this calculus. This will give non-expert users and developers the ability to obtain implemented provers with relative ease in a supported way. For the user crucially this removes the burden of being concerned with proving soundness, completeness and decidability results, and implementing or adapting a prover.We will extend the theoretical foundation of the framework in various ways in order to make it more comprehensive and extend the scope of tableau methods as decision procedures. A series of tools will be developed: a tableau prover generator program and auxiliary software to ensure reliability, correctness and efficiency of the generator and the generated provers. To allow for the rapid employment of the technology and receive feedback from users a first prototype will be completed and released within one year and two tutorials will be organised. Several case studies will be conducted with the prototype to identify important issues that may need to be changed and improved in the prototype. Areas where it is crucial to find optimisations are rule refinement, prover efficiency, and generalisation of the framework. To quantify the success of the project, the utility of the developed tools and the generated provers, the acceptance by users and the practical benefit of generated provers an evaluation will be conducted.Overall, automated prover generation is a new and difficult research problem, but we believe that it is now a real possibility that we intend to realise in this project.