Deciding the Word Problem in the Union of Equational Theories Sharing Constructors

Franz Baader; Cesare Tinelli

doi:10.1007/3-540-48685-2_14

Back

Deciding the Word Problem in the Union of Equational Theories Sharing Constructors

Book chapter

Peer reviewed

Deciding the Word Problem in the Union of Equational Theories Sharing Constructors

Franz Baader and Cesare Tinelli

Rewriting Techniques and Applications, pp.175-189

Lecture Notes in Computer Science, Springer Berlin Heidelberg

11/05/1999

DOI: 10.1007/3-540-48685-2_14

View Online

Abstract

The main contribution of this paper is a new method for combining decision procedures for the word problem in equational the- ories sharing “constructors.” The notion of constructors adopted in this paper has a nice algebraic definition and is more general than a related notion introduced in previous work on the combination problem.

Decision Procedure

Equational Theory

Free Algebra

Normal Form

Word Problem

Details

Title: Subtitle: Deciding the Word Problem in the Union of Equational Theories Sharing Constructors
Creators: Franz Baader - RWTH Aachen University
Cesare Tinelli - University of Illinois Urbana-Champaign
Resource Type: Book chapter
Publication Details: Rewriting Techniques and Applications, pp.175-189
Publisher: Springer Berlin Heidelberg; Berlin, Heidelberg
Series: Lecture Notes in Computer Science
DOI: 10.1007/3-540-48685-2_14
eISSN: 1611-3349
ISSN: 0302-9743
Language: English
Date published: 11/05/1999
Academic Unit: Computer Science
Record Identifier: 9984259502602771

Metrics

4 Record Views