Abstract
In this paper we present an approach to reasoning with large theories which is based on the abstraction-refinement framework. The proposed approach consists of the following approximations: the over-approximation, the under-approximation and their combination. We present several concrete abstractions based on subsumption, signature grouping and argument filtering. We implemented our approach in a theorem prover for first-order logic iProver and evaluated over the TPTP library.
Author supplied keywords
Cite
CITATION STYLE
Lopez Hernandez, J. C., & Korovin, K. (2018). An Abstraction-Refinement Framework for Reasoning with Large Theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 663–679). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
