An abstraction-refinement framework for reasoning with large theories
Authors: Julio Cesar Lopez Hernandez and Konstantin Korovin
Paper Information
| Title: | An abstraction-refinement framework for reasoning with large theories |
| Authors: | Julio Cesar Lopez Hernandez and Konstantin Korovin |
| Proceedings: | IJCAR Proceedings 9th IJCAR, 2018 |
| Editors: | Stephan Schulz, Didier Galmiche and Roberto Sebastiani |
| Keywords: | theorem proving, abstraction-refinement, large theories |
| Abstract: | ABSTRACT. In this paper we present an abstraction-refinement framework for reasoning with large theories. We consider several types of abstractions based on over and under approximations of first-order theories. We implemented the proposed approached in a theorem prover iProver and evaluated over the TPTP library. |
| Pages: | 16 |
| Talk: | Jul 17 12:00 (Session 119D: AR Miscellanea) |
| Paper: |  |