An abstraction-refinement framework for reasoning with large theories.

Julio Cesar Lopez Hernandez; Konstantin Korovin

doi:10.1007/978-3-319-94205-6_43

An abstraction-refinement framework for reasoning with large theories.

Julio Cesar Lopez Hernandez, Konstantin Korovin

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

71 Downloads (Pure)

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 the-
orem prover for first-order logic iProver and evaluated over the TPTP
library.

Original language	English
Title of host publication	IJCAR 2018: Automated Reasoning
Pages	663-679
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-319-94205-6_43
Publication status	Published - 30 Jun 2018
Event	9th International Joint Conference on Automated Reasoning - University of Oxford, Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018 Conference number: 9 http://ijcar2018.org/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Joint Conference on Automated Reasoning
Abbreviated title	IJCAR
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18
Internet address	http://ijcar2018.org/

Keywords

Automated Reasoning

Access to Document

10.1007/978-3-319-94205-6_43

abstr_ref_ijcar_2018Accepted author manuscript, 485 KB

http://www.cs.man.ac.uk/~korovink/my_pub/abstr_ref_ijcar_2018.pdf

Cite this

@inproceedings{74723103e12049dbbe2668d2cd16297d,

title = "An abstraction-refinement framework for reasoning with large theories.",

abstract = "In this paper we present an approach to reasoning withlarge theories which is based on the abstraction-refinement framework.The proposed approach consists of the following approximations: theover-approximation, the under-approximation and their combination. Wepresent several concrete abstractions based on subsumption, signaturegrouping and argument filtering. We implemented our approach in a the-orem prover for first-order logic iProver and evaluated over the TPTPlibrary.",

keywords = "Automated Reasoning",

author = "{Lopez Hernandez}, {Julio Cesar} and Konstantin Korovin",

year = "2018",

month = jun,

day = "30",

doi = "10.1007/978-3-319-94205-6_43",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "663--679",

booktitle = "IJCAR 2018: Automated Reasoning",

note = "9th International Joint Conference on Automated Reasoning , IJCAR ; Conference date: 14-07-2018 Through 17-07-2018",

url = "http://ijcar2018.org/",

}

TY - GEN

T1 - An abstraction-refinement framework for reasoning with large theories.

AU - Lopez Hernandez, Julio Cesar

AU - Korovin, Konstantin

N1 - Conference code: 9

PY - 2018/6/30

Y1 - 2018/6/30

N2 - In this paper we present an approach to reasoning withlarge theories which is based on the abstraction-refinement framework.The proposed approach consists of the following approximations: theover-approximation, the under-approximation and their combination. Wepresent several concrete abstractions based on subsumption, signaturegrouping and argument filtering. We implemented our approach in a the-orem prover for first-order logic iProver and evaluated over the TPTPlibrary.

AB - In this paper we present an approach to reasoning withlarge theories which is based on the abstraction-refinement framework.The proposed approach consists of the following approximations: theover-approximation, the under-approximation and their combination. Wepresent several concrete abstractions based on subsumption, signaturegrouping and argument filtering. We implemented our approach in a the-orem prover for first-order logic iProver and evaluated over the TPTPlibrary.

KW - Automated Reasoning

UR - https://link.springer.com/chapter/10.1007/978-3-319-94205-6_43

U2 - 10.1007/978-3-319-94205-6_43

DO - 10.1007/978-3-319-94205-6_43

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 663

EP - 679

BT - IJCAR 2018: Automated Reasoning

T2 - 9th International Joint Conference on Automated Reasoning

Y2 - 14 July 2018 through 17 July 2018

ER -

An abstraction-refinement framework for reasoning with large theories.

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this