Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Lynch, Christopher
Tran, Duc-Khanh

dblp
dblp

Not MPG Author(s):

Lynch, Christopher

Editor(s):

Cha, Sungdeok (Steve)
Choi, Jin-Young
Kim Moonzoo
Lee, Insup
Viswanathan, Mahesh

dblp
dblp
dblp
dblp
dblp

Not MPII Editor(s):

Cha, Sungdeok (Steve)
Choi, Jin-Young
Kim Moonzoo
Lee, Insup
Viswanathan, Mahesh

BibTeX cite key*:

tran-atva08

Title, Booktitle

Title*:

SMELS: Satisfiability Modulo Equality with Lazy Superposition

Booktitle*:

Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008

Event, URLs

URL of the conference:

http://pswlab.kaist.ac.kr/atva2008/

URL for downloading the paper:

http://www.springerlink.com/content/x58h1487t724k2l0/

Event Address*:

Seoul, Korea

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

20 October 2008

Event End Date:

23 October 2008

Publisher

Name*:

Springer

URL:

http://www.springer-ny.com/

Address*:

Berlin / Heidelberg

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

5311

Number:


Month:


Pages:

186-200

Year*:

2008

VG Wort Pages:


ISBN/ISSN:

0302-9743

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

We give a method for extending efficient SMT solvers to handle quantifiers, using Superposition inference rules. In our method, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SMT solver, which runs a DPLL method to build partial models. The partial model is passed to a Congruence Closure procedure, as is normally done in SMT. Congruence Closure calculates all reduced (dis)equations in the partial model and passes them to a Superposition procedure, along with a justification. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the (dis)equations and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of this method, using a nontrivial modification of Bachmair and Ganzinger’s model generation technique. We believe this combination uses the best of both worlds, an SMT process to handle ground clauses efficiently, and a Superposition procedure which uses orderings to handle the nonground clauses.

URL for the Abstract:

http://www.springerlink.com/content/x58h1487t724k2l0/



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{tran-atva08,
AUTHOR = {Lynch, Christopher and Tran, Duc-Khanh},
EDITOR = {Cha, Sungdeok (Steve) and Choi, Jin-Young and Kim Moonzoo and Lee, Insup and Viswanathan, Mahesh},
TITLE = {{SMELS}: Satisfiability Modulo Equality with Lazy Superposition},
BOOKTITLE = {Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008},
PUBLISHER = {Springer},
YEAR = {2008},
VOLUME = {5311},
PAGES = {186--200},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Seoul, Korea},
ISBN = {0302-9743},
}


Entry last modified by Uwe Waldmann, 03/01/2013
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Viorica Sofronie-Stokkermans
Created
03/06/2009 12:59:09 PM
Revisions
2.
1.
0.

Editor(s)
Uwe Waldmann
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans

Edit Dates
01.03.2013 11:25:25
03/06/2009 12:59:53 PM
03/06/2009 12:59:09 PM

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section