An abstraction-refinement framework for first-order reasoning with large theories

In this thesis, we investigate an abstraction-refinement framework for first-order reasoning with application to large theories. Efficient reasoning with large theories is one of the main challenges in automated theorem proving because of the difficulty of dealing with the combinatorial explosion of the search space. The use of large theories encompasses different applications ranging from reasoning with ontologies, or another type of knowledge bases, to proof assistants for mathematics. Our proposed approach uses the abstraction-refinement framework to deal with the complexity of large theories. Moreover, it encompasses two ways to approximate the original theory by under- and over-approximations. The proposed framework allows the combination of both approximations. Thus, such combination can converge rapidly to proof if it exists or to disprove the conjecture. Another characteristic of our approach is that it interleaves the abstraction-refinement process and the reasoning phase to have a dynamic interaction between them. Finally, we implemented the proposed abstraction-refinement framework and integrated it into a state-of-the-art automatic theorem prover iProver.