MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Ganzinger, Harald
Korovin, Konstantin		dblp
dblp
Editor(s):
Kolaitis, Phokiondblp
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
Conference URL::
http://www.dcs.ed.ac.uk/home/als/lics/lics03/
Downloading URL:
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:
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, 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, 03/12/2010
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/29/2003 08:45:00 PM
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

File Attachment Icon
_03LICS.pdf