Automating Coherent Logic

We propose to build an automated reasoning system for first-order logic (FOL) by translating reasoning problems to a fragment of FOL called coherent logic (CL) and then solving them by a fast problem solver for CL. Both the translation and the fast CL so lver are to be developed in the project. Automated reasoning in FOL is an established research field with many applications in mathematics, logic and computer science (e.g., the verification of hard- and software, deductive databases, semantic web appli cations etc.) The strong point of CL as compared to weaker logics (for example, resolution logic) is that CL has both quantifiers ("for all" and "there exists") together with a simple proof procedure. Due to this expressiveness problems can be directly or equivalently formulated in CL so that the problem solver works on essentially the same problem as the user. The advantages of this approach are: - strong support for interactive problem solving; - explanation of solutions found by the system is facil itated (of crucial importance for many applications); - some inefficiencies inherent to the translation of FOL to weaker logics than CL are avoided. A novel feature of the proposed system is that it will generate proof objects, that is, detailed formal d escriptions of solutions found, which can be imported and used by logical frameworks such as Coq, Isabelle and Agda. Proof objects are important for explanation, independent verification and they increase the level of automation of the logical framework i n a significant way.