Name
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. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-94205-6_43 | Lecture Notes in Artificial Intelligence |
Keywords | DocType | Volume |
Automated reasoning,Large theories,Abstraction-refinement | Conference | 10900 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Julio Cesar Lopez Hernandez | 1 | 0 | 0.34 |
| Konstantin Korovin | 2 | 288 | 20.64 |