Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne		dblp
dblp
dblp
dblp

BibTeX cite key*:

Bachmair-et-al-95-ic

Title

Title*:

Basic Paramodulation

Journal

Journal Title*:

Information and Computation
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Academic Press
Publisher's URL:


Publisher's
Address:


ISSN:

0890-5401

Vol, No, pp, Date

Volume*:

121
Number:

2

Publishing Date:

1995

Pages*:

172-192
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:

Revised version of TR MPI-I-93-236, 1993

(LaTeX) Abstract:

We introduce a class of restrictions for the
ordered paramodulation and superposition calculi (inspired by the {\em basic\/}
strategy for narrowing), in which paramodulation inferences are forbidden at
terms introduced by substitutions from previous inference steps.
In addition we introduce restrictions based on term selection rules and
redex orderings, which are general criteria for delimiting the terms
which are available for inferences. These refinements are compatible
with standard ordering restrictions and are complete without paramodulation
into variables or using functional reflexivity axioms.
We prove refutational completeness in the context of deletion rules,
such as simplification by rewriting (demodulation) and subsumption,
and of techniques for eliminating redundant inferences.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography


BibTeX Entry:
@ARTICLE{Bachmair-et-al-95-ic,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Lynch, Christopher and Snyder, Wayne},
 TITLE = {Basic Paramodulation},
 JOURNAL = {Information and Computation},
 PUBLISHER = {Academic Press},
 YEAR = {1995},
 NUMBER = {2},
 VOLUME = {121},
 PAGES = {172--192},
 ISBN = {0890-5401},
 NOTE = {Revised version of TR MPI-I-93-236, 1993},
}

Entry last modified by Uwe Brahm, 03/12/2010
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)
Christine Kiesel		Created
01/04/1998 10:31:36 PM
Revisions
3.
2.
1.
0.
Editor(s)
Uwe Brahm
Christine Kiesel
Uwe Brahm/MPII/DE
Christine Kiesel/AG2/MPII/DE
Edit Dates
07.01.97 02:52:53
06/01/97 16:19:31
20.03.96 18:34:40
01/02/96 12:27:49