The term rewriting approach to automated theorem proving

DOI10.1016/0743-1066(92)90047-7zbMath0754.68100OpenAlexW2037405229MaRDI QIDQ4015952

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

Publication date: 10 November 1992

Published in: The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0743-1066(92)90047-7

zbMATH Keywords

equational logiccompletionterminationrefutationBoolean ringparamodulationconditional rewritingequational unificationequational rewritingHorn clause logic with equalityinductive theoremsfirst order logic with equality

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42)

Related Items

More problems in rewriting, Towards automated deduction in cP systems, A categorical critical-pair completion algorithm