Existential and positive theories of equations in graph products

DOI10.1007/S00224-003-1110-XMaRDI QIDQ705067zbMATH OpenOpenAlexFDO

Authors Volker Diekert, Markus Lohrey

Publication date 25 January 2005

Published in Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00224-003-1110-x

zbMATH Keywords

complexitydecidabilityexistential theoryfree groupsfree monoidsgraph productpositive theoryPSPACEtrace monoid

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Word problems, other decision problems, connections with logic and automata (group-theoretic aspects) (20F10) Free semigroups, generators and relations, word problems (20M05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

Review text

In this article it is proved that, for a fixed graph product \(\mathbb P\) of finite monoids, free monoids, and free groups, the existential (i.e., sentences in prenex normal form without universal quantifiers) theory of equations can be decided in PSPACE. Moreover, when the equations have normalized rational (NRAT\((\mathbb P)\)) constraints, the problem becomes PSPACE-complete. Another main result states that, for graph products of finite and free groups, the positive (i.e., sentences without negations) theory of equations with recognizible (REC\((\mathbb G)\)) constraints is decidable. These results continue the stream of research on decidability of theories of equations on monoids and groups started by \textit{G. S. Makanin} [Mat. Sb., Nov. Ser. 103(145), 147--236 (1977; Zbl 0371.20047)]. The results in this paper are based on the main result of \textit{V. Diekert} and \textit{A. Muscholl} [Lect. Notes Comput. Sci. 2076, 543--554 (2001; Zbl 0986.20036)] on existential theories of equations in trace monoids with involution. This result is used within the underlying trace monoid with involution of the graph product. It is proved that, for an existential sentence \(\phi\) with constraints in NRAT\((\mathbb P)\), there exist an existential sentence \(\phi'\) such that \(\phi\) holds in \(\mathbb P\) if and only if \(\phi'\) holds in the underlying monoid with involution. In this reduction, a specific confluent trace rewriting systems is used. The decidability of the positive theory of equations with constraints in REC\((\mathbb G)\), where \(\mathbb G\) is a graph product of finite and free groups, is proved in two steps. Firstly, it is proved that it possible to restrict the investigation to graph products of a particular type, and, secondly, the positive sentences with constraints in REC are reduced to existential sentences with constraints in NRAT. The result then follows by the first result.

Recommendations

• scientific article; zbMATH DE number 2086411
• On the generic existential theory of finite graphs
• Equational theory of relation algebras with positive operations
• The Equational Logic For Graph Algebras
• Graph products of completely positive maps
• scientific article; zbMATH DE number 1047921
• Equivalence proof for intuitionistic existential alpha graphs
• A note on equational theories
• On the equational graphs over finite fields
• Positive model theory and amalgamations

Cited in

(13)

• First-order aspects of Coxeter groups
• Equations in groups that are virtually direct products
• The existential theory of equations with rational constraints in free groups is PSPACE-complete
• On systems of equations over free partially commutative groups.
• SOLVABILITY OF EQUATIONS IN GRAPH GROUPS IS DECIDABLE
• WORD EQUATIONS OVER GRAPH PRODUCTS
• scientific article; zbMATH DE number 1754619 (Why is no real title available?)
• scientific article; zbMATH DE number 2086411 (Why is no real title available?)
• A NOTE ON THE EXISTENTIAL THEORY OF EQUATIONS IN PLAIN GROUPS
• The Diophantine problem in some metabelian groups
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
• Logical aspects of Cayley-graphs: the group case

This page was built for publication: Existential and positive theories of equations in graph products

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q705067)