Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Union of Finitely Generated Congruences on Ground Term Algebra

Sándor Vágvölgyi

Abstract

We show that for any ground term equation systems $E$ and $F$, (1) the union of the generated congruences by $E$ and $F$ is a congruence on the ground term algebra if and only if there exists a ground term equation system $H$ such that the congruence generated by $H$ is equal to the union of the congruences generated by $E$ and $F$ if and only if the congruence generated by the union of $E $ and $F$ is equal to the union of the congruences generated by $E $ and $F$, and (2) it is decidable in square time whether the congruence generated by the union of $E$ and $F$ is equal to the union of the congruences generated by $E $ and $F$, where the size of the input is the number of occurrences of symbols in $E$ plus the number of occurrences of symbols in $F$.

Union of Finitely Generated Congruences on Ground Term Algebra

Abstract

We show that for any ground term equation systems and , (1) the union of the generated congruences by and is a congruence on the ground term algebra if and only if there exists a ground term equation system such that the congruence generated by is equal to the union of the congruences generated by and if and only if the congruence generated by the union of and is equal to the union of the congruences generated by and , and (2) it is decidable in square time whether the congruence generated by the union of and is equal to the union of the congruences generated by and , where the size of the input is the number of occurrences of symbols in plus the number of occurrences of symbols in .

Paper Structure

This paper contains 29 sections, 69 theorems, 4 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Algorithm concepts
  4. Basic notions
  5. Sets and Relations baader1999term
  6. Ground terms baader1999term
  7. Ground term rewrite systems and equation systems jsc/Snyder93
  8. Bottom-up tree automata Engelfriet75, gs
  9. Directed pseudographs without parallel arcs bang
  10. Congruence closure on subterm dags jsc/Snyder93
  11. Running Examples for the Main Cases
  12. Fast Ground Completion Introducing Additional Constants
  13. Running Examples Continued
  14. The Auxiliary dpwpa for the GTESs $E$ and $F$
  15. Running Examples Further Continued
  16. ...and 14 more sections

Key Result

Proposition 2.1

cormen The search operation takes $O(\mathrm{log}\, n)$ time on a red-black tree, where $n$ is the size of the tree.

Theorems & Definitions (178)

  • Proposition 2.1
  • Proposition 2.2
  • proof
  • Definition 2.3: johnsonbaugh
  • Proposition 2.4: baader1999term
  • proof
  • Definition 2.6
  • Proposition 2.9: jsc/Snyder93
  • Definition 2.10
  • Proposition 2.11
  • ...and 168 more