Automated Prover Generation

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

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.