Deciding the Word Problem in the Union of Equational Theories

Franz Baader; Cesare Tinelli

doi:10.1006/inco.2001.3118

Back

Deciding the Word Problem in the Union of Equational Theories

Journal article

Open access

Peer reviewed

Deciding the Word Problem in the Union of Equational Theories

Franz Baader and Cesare Tinelli

Information and computation, Vol.178(2), pp.346-390

2002

DOI: 10.1006/inco.2001.3118

Files and links (1)

url

https://doi.org/10.1006/inco.2001.3118View

Published (Version of record) Open Access

Abstract

The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, this method is based on transformation rules. Furthermore, it is not limited to theories with disjoint signatures but it also applies to theories sharing constructors.

equational reasoning

combination of decision procedures

word problem

Details

Title: Subtitle: Deciding the Word Problem in the Union of Equational Theories
Creators: Franz Baader - RWTH Aachen University
Cesare Tinelli - University of Iowa
Resource Type: Journal article
Publication Details: Information and computation, Vol.178(2), pp.346-390
DOI: 10.1006/inco.2001.3118
ISSN: 0890-5401
eISSN: 1090-2651
Publisher: Elsevier Inc
Language: English
Date published: 2002
Academic Unit: Computer Science
Record Identifier: 9984259432902771

Metrics

5 Record Views

20 Times Cited - Web of Science