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):

Ganzinger, Harald
Korovin, Konstantin

dblp
dblp



Editor(s):

Kolaitis, Phokion

dblp

Not MPII Editor(s):

Kolaitis, Phokion

BibTeX cite key*:

GanzingerKorovin-03-lics

Title, Booktitle

Title*:

New Directions in Instantiation-Based Theorem Proving


_03LICS.pdf (135.87 KB)

Booktitle*:

18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)

Event, URLs

URL of the conference:

http://www.dcs.ed.ac.uk/home/als/lics/lics03/

URL for downloading the paper:

http://www.mpi-sb.mpg.de/~hg/pca.html#_03LICS

Event Address*:

Ottawa, Canada

Language:

English

Event Date*
(no longer used):

old

Organization:

Institute of Electrical and Electronics Engineers (IEEE)

Event Start Date:

8 May 2003

Event End Date:

12 May 2003

Publisher

Name*:

IEEE

URL:

http://www.ieee.org/

Address*:

Los Alamitos, USA

Type:


Vol, No, Year, pp.

Series:


Volume:


Number:


Month:


Pages:

55-64

Year*:

2003

VG Wort Pages:

10

ISBN/ISSN:

0-7695-1884-2

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

We consider instantiation-based theorem proving whereby
instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests.
We give a model construction proof of completeness by which restrictive inference
systems as well as admissible simplification techniques can be
justified. Another contribution of the paper are novel inference
systems that allow one to also employ decision procedures for
first-order fragments more complex than propositional logic.
The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of
successively refining the approximation.



Download
Access Level:

Public

Correlation

MPG Unit:




MPG Subunit:


Appearance:

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



BibTeX Entry:

@INPROCEEDINGS{GanzingerKorovin-03-lics,
AUTHOR = {Ganzinger, Harald and Korovin, Konstantin},
EDITOR = {Kolaitis, Phokion},
TITLE = {New Directions in Instantiation-Based Theorem Proving},
BOOKTITLE = {18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)},
PUBLISHER = {IEEE},
YEAR = {2003},
ORGANIZATION = {Institute of Electrical and Electronics Engineers (IEEE)},
PAGES = {55--64},
ADDRESS = {Ottawa, Canada},
ISBN = {0-7695-1884-2},
}


Entry last modified by Christine Kiesel, 04/20/2009
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)
Konstantin Korovin
Created
04/20/2009 10:19:07 AM
Revisions
12.
11.
10.
9.
8.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
17.06.2004 15:50:41
17.06.2004 15:33:40
26.01.2004 12:07:27
26.01.2004 12:01:01
01/22/2004 08:08:44 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
_03LICS.pdf