Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | 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