Electronic Proceedings Article
@InProceedings
Internet-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):

de Nivelle, Hans
Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare

dblp
dblp
dblp
dblp

Not MPG Author(s):

Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare

Editor(s):

Ahrendt, Wolfgang
Baumgartner, Peter
de Nivelle, Hans

dblp
dblp
dblp

Not MPII Editor(s):

Ahrendt, Wolfgang
Baumgartner, Peter

BibTeX cite key*:

deNivelle2006b

Title, Conference

Title*:

Computing Finite Models by Reduction to Function-Free Clause Logic

Booktitle*:

IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability

Event Address*:

Seattle, USA

URL of the conference:

http://www.easychair.org/FLoC-06/DISPROVING.html

Event Date*:
(no longer used):


URL for downloading the paper:

http://www.easychair.org/FLoC-06/DISPROVING-preproceedings.pdf

Event Start Date:

16 August 2006

Event End Date:

16 August 2006

Language:

English

Organization:


Publisher

Publisher's Name:

The 2006 Federated Logic Conference

Publisher's URL:


Address*:

Seattle, USA

Type:


Vol, No, pp., Year

Series:


Volume:


Number:


Month:

August

Pages:

82-95



Sequence Number:


Year*:

2006

ISBN/ISSN:






Abstract, Links, ©

URL for Reference:


Note:


(LaTeX) Abstract:

We propose to reduce model search to a sequence of satisfiability
problems made of function-free clause sets, and to apply
efficient theorem provers capable of deciding such problems on
them.
The main motivation for this method is the fact that
first-order clause sets
grow more slowly than their propositional counterparts, thus
allowing for more space-efficient reasoning.
We describe the method in detail, and show how it is integrated
into Darwin, which is an implementation of the model evolution
calculus. Although we used Darwin, the results are general,
as our approach can be used
in principle with every system that decides the satisfiability
of function-free first-order clause sets.

URL for the Abstract:




Tags, Categories, Keywords:

theorem proving, finite model search

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

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

BibTeX Entry:
@INPROCEEDINGS{deNivelle2006b,
AUTHOR = {de Nivelle, Hans and Baumgartner, Peter and Fuchs, Alexander and Tinelli, Cesare},
EDITOR = {Ahrendt, Wolfgang and Baumgartner, Peter and de Nivelle, Hans},
TITLE = {Computing Finite Models by Reduction to Function-Free Clause Logic},
BOOKTITLE = {IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability},
PUBLISHER = {The 2006 Federated Logic Conference},
YEAR = {2006},
PAGES = {82--95},
ADDRESS = {Seattle, USA},
MONTH = {August},
}


Entry last modified by Christine Kiesel, 01/28/2008
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)
Hans de Nivelle
Created
09/25/2006 12:36:22 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
26.02.2007 16:01:34
17.02.2007 09:19:06
15.02.2007 17:00:17
15.02.2007 16:57:32
09/25/2006 12:38:20 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section