×
Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël

The term rewriting approach to automated theorem proving. (English) Zbl 0754.68100

J. Log. Program. 14, No. 1-2, 71-99 (1992).
We give a survey of different methods developed in term rewriting for application to automated deduction in various logical systems.

Cited in 3 Documents

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems
68-02 Research exposition (monographs, survey articles) pertaining to computer science

Keywords:

equational logic; termination; completion; inductive theorems; equational rewriting; equational unification; Horn clause logic with equality; conditional rewriting; refutation; first order logic with equality; paramodulation; Boolean ring
Cite Review PDF
Full Text: DOI