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 solver 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 applications etc.) The advantages of the use of CL instead of weaker logics (for example, resolution logic) are: strong support for interactive problem solving and for explanation facilities, which is of crucial importance for many applications. Moreover, some inefficiencies inherent to the translation of FOL to weaker logics than CL are avoided.

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Marc Bezem, Thierry Coquand
• Keywords: Automated Reasoning, Fast Cl Solver, Logics, LPAR 2005