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

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