Emma@SU-CSLI.ARPA (Emma Pease) (01/23/86)
[Excerpted from the CSLI Newsletter by Laws@SRI-AI.]
CSLI ACTIVITIES FOR NEXT THURSDAY, January 30, 1986
2:15 p.m. CSLI Seminar
Ventura Hall Term Rewriting Systems and Application to Automated
Trailer Classroom Theorem Proving and Logic Programming
Helene Kirchner (Kirchner@sri-ai)
Term Rewriting Systems and Application to
Automated Theorem Proving and Logic Programming
Helene Kirchner
Term rewriting systems are sets of rules (i.e. directed equations)
used to compute equivalent terms in an equational theory. Term
rewriting systems are required to be terminating and confluent in
order to ensure that any computation terminates and does not depend on
the choice of applied rules. Completion of term rewriting systems
consists of building, from a set of non-directed equations, a
confluent and terminating set of rules that has the same deductive
power. After a brief description of these two notions, their
application in two different domains are illustrated:
- automated theorem proving in equational and first-order
logic,
- construction of interpretors for logic programming languages
mixing relational and functional features.