MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Ganzinger, Harald
Meyer, Christoph
Weidenbach, Christoph
dblp
dblp
dblp
Editor(s):
McCune, Williamdblp
BibTeX cite key*:
GanzingerMeyerWeidenbach-97-cade
Title, Booktitle
Title*:
Soft Typing for Ordered Resolution
Booktitle*:
Proceedings of the 14th International Conference on Automated Deduction (CADE-14)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Townsville, Australia
Language:
English
Event Date*
(no longer used):
July, 14-17
Organization:
Event Start Date:
17 May 2021
Event End Date:
17 May 2021
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
1249
Number:
Month:
Pages:
321-335
Year*:
1997
VG Wort Pages:
ISBN/ISSN:
3-540-63104-6
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We propose a variant of ordered resolution with semantic restrictions
based on interpretations which are identified by the given atom ordering
and selection function. Techniques for effectively approximating validity
in these interpretations are described that are related to methods of
soft typing for programming languages.
The framework is shown to be strictly more general than certain related
methods.
Implementation in the \spass\ prover has lead to encouraging experimental
results.
HyperLinks / References / URLs:
http://www.mpi-sb.mpg.de/\~{}hg/pca.html\#CADE97
Download
Access Level:

Correlation
MPG Unit:
MPG Subunit:
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography



BibTeX Entry:

@INPROCEEDINGS{GanzingerMeyerWeidenbach-97-cade,
AUTHOR = {Ganzinger, Harald and Meyer, Christoph and Weidenbach, Christoph},
EDITOR = {McCune, William},
TITLE = {Soft Typing for Ordered Resolution},
BOOKTITLE = {Proceedings of the 14th International Conference on Automated Deduction (CADE-14)},
PUBLISHER = {Springer},
YEAR = {1997},
VOLUME = {1249},
PAGES = {321--335},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Townsville, Australia},
ISBN = {3-540-63104-6},
}


Entry last modified by Christine Kiesel, 05/12/2006
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)
Harald Ganzinger
Created
05/12/2006 04:46:38 PM
Revisions
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Christine Kiesel
Uwe Brahm
Harald Ganzinger
Edit Dates
27/01/98 12:06:06
27/01/98 11:46:45
09.05.97 15:00:11
21/04/97 15:50:51