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		dblp
dblp

BibTeX cite key*:

BachmairGanzinger-94-jlc

Title

Title*:

Rewrite-based equational theorem proving with selection and simplification

Journal

Journal Title*:

Journal of Logic and Computation
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Oxford University Press
Publisher's URL:


Publisher's
Address:


ISSN:

0955-792X

Vol, No, pp, Date

Volume*:

4
Number:

3

Publishing Date:

1994

Pages*:

217-247
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:

Revised version of Technical Report MPI-I-91-208, 1991

(LaTeX) Abstract:

We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutation completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses. We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses during the theorem proving process preserves refutation completeness. It is often possible to compute the closure of nontrivial sets of clauses under application of non-redundant inferences. The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular one can restrict attention to proofs that have support from the goals without compromising refutation completeness. Additional syntactic properties allow to restrict the search space even further, as we demonstrate for so-called quasi-Horn clauses. The results in this paper contain as special cases or generalize many known results about Knuth-Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses over built-in Booleans), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.

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:
CCL bibliography


BibTeX Entry:
@ARTICLE{BachmairGanzinger-94-jlc,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
 TITLE = {Rewrite-based equational theorem proving with selection and simplification},
 JOURNAL = {Journal of Logic and Computation},
 PUBLISHER = {Oxford University Press},
 YEAR = {1994},
 INSTITUTION = {Max-Planck-Institut für Informatik},
 NUMBER = {3},
 VOLUME = {4},
 PAGES = {217--247},
 ISBN = {0955-792X},
 NOTE = {Revised version of Technical Report MPI-I-91-208, 1991},
}

Entry last modified by Christine Kiesel, 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)
Harald Ganzinger		Created
01/22/1995 02:33:10 PM
Revisions
15.
14.
13.
12.
11.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
03.09.2001 16:55:06
26/04/99 11:40:06
26/04/99 11:09:44
26/04/99 11:05:49
30/01/96 13:18:59