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:




Library Locked Library locked




Author, Editor

Author(s):

Burel, Guillaume

dblp



Editor(s):

Dawar, Anuj
Veith, Helmut

dblp
dblp

Not MPII Editor(s):

Dawar, Anuj
Veith, Helmut

BibTeX cite key*:

Burel2010

Title, Booktitle

Title*:

Embedding Deduction Modulo into a Prover

Booktitle*:

Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL

Event, URLs

URL of the conference:

http://mfcsl2010.fi.muni.cz/csl

URL for downloading the paper:

http://www.springerlink.com/content/0g30v1n222448385/fulltext.pdf

Event Address*:

Brno, Czech Republic

Language:

English

Event Date*
(no longer used):


Organization:

European Association for Computer Science Logic (EACSL)

Event Start Date:

23 August 2010

Event End Date:

27 August 2010

Publisher

Name*:

Springer

URL:

http://www.springer.com/

Address*:

Berlin

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

6247

Number:


Month:

August

Pages:

155-169

Year*:

2010

VG Wort Pages:


ISBN/ISSN:

978-3-642-15204-7

Sequence Number:


DOI:

10.1007/978-3-642-15205-4



Note, Abstract, ©


(LaTeX) Abstract:

Deduction modulo consists in presenting a theory through rewrite
rules to support automatic and interactive proof search. It induces
proof search methods based on narrowing, such as the polarized
resolution modulo. We show how to combine this method with more
traditional ordering restrictions. Interestingly, no compatibility
between the rewriting and the ordering is requested to ensure
completeness. We also show that some simplification rules, such as
strict subsumption eliminations and demodulations, preserve
completeness. For this purpose, we use a new framework based on a
proof ordering. These results show that polarized resolution modulo
can be integrated into existing provers, where these restrictions
and simplifications are present. We also discuss how this
integration can actually be done by diverting the main algorithm of
state-of-the-art provers.

URL for the Abstract:

http://www.springerlink.com/content/0g30v1n222448385/

Keywords:

automated deduction, term rewriting, ordered resolution, syntactic completeness proof, set-of-support strategy

HyperLinks / References / URLs:

http://www.springerlink.com/content/0g30v1n222448385/



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

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



BibTeX Entry:

@INPROCEEDINGS{Burel2010,
AUTHOR = {Burel, Guillaume},
EDITOR = {Dawar, Anuj and Veith, Helmut},
TITLE = {Embedding Deduction Modulo into a Prover},
BOOKTITLE = {Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL},
PUBLISHER = {Springer},
YEAR = {2010},
ORGANIZATION = {European Association for Computer Science Logic (EACSL)},
VOLUME = {6247},
PAGES = {155--169},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Brno, Czech Republic},
MONTH = {August},
ISBN = {978-3-642-15204-7},
DOI = {10.1007/978-3-642-15205-4},
}


Entry last modified by Anja Becker, 02/07/2011
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)
[Library]
Created
12/03/2010 09:14:32 AM
Revision
1.
0.


Editor
Anja Becker
Guillaume Burel


Edit Date
07.02.2011 10:17:57
12/03/2010 09:14:32 AM


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