File:Solving the word problem without and with completion.pdf

From Wikimedia Commons, the free media repository
Jump to navigation Jump to search

Original file(1,210 × 1,240 pixels, file size: 9 KB, MIME type: application/pdf)


Add a one-line explanation of what this file represents



English: Shows a simplified example of the search space for deciding the word problem, i.e., given a set E of equations and two terms s,t (represented by the left- and rightmost vertice), to decide if s=t follows from E. Proof search usually runs into dead ends (red paths); to find a valid proof (green path) may be infeasible without human intuition. However, if the Knuth-Bendix completion algorithm was able to compute from E an equivalent confluent (and terminating) term rewriting system R (shadow paths), deciding if s=t is simple: apply rules from R to s as long as possible to obtain a term s’ (s’ is unique, no matter in which the order rules are applied), rewrite t to some t’ in a similar way, then s=t if and only if s’=t’.


Own work


Jochen Burghardt

Other versions

File:Solving the word problem without and with completion svg.svg

LaTeX source Code

%%%%% labyrinth convenience macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcounter{curX}       % current x coordinate (in unit lengths)
\newcounter{curY}       % current y coordinate (in unit lengths)

% dir{X}{Y}: advance line in direction 10*X,10*Y

% \go{X}{Y}: start line at X,Y

% windrose commands

%%%%% colors %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\definecolor{cSuc}      {rgb}{0.00,0.50,0.00}   % successful eqn proof
\definecolor{cFai}      {rgb}{0.99,0.30,0.30}   % failed eqn proof attempts
\definecolor{cAvl}      {rgb}{0.90,0.90,0.90}   % available rewrites
\definecolor{cUse}      {rgb}{0.40,0.40,0.40}   % used rewrites

% confluent and terminating rewriting system
% actually used to compute normal forms
\put(20,97){\circle*{2}}%                       left
\put(170,107){\circle*{2}}%                     right
\put(100,-4){\circle*{2}}%                      normal form

% unsuccessful equations
% successful equations


I, the copyright holder of this work, hereby publish it under the following license:
w:en:Creative Commons

attribution share alike

This file is licensed under the Creative Commons Attribution-Share Alike 3.0 Unported license.
You are free:
  • to share – to copy, distribute and transmit the work
  • to remix – to adapt the work
Under the following conditions:
  • attribution – You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
  • share alike – If you remix, transform, or build upon the material, you must distribute your contributions under the same or compatible license as the original.

File history

Click on a date/time to view the file as it appeared at that time.

current14:02, 9 June 2014Thumbnail for version as of 14:02, 9 June 20141,210 × 1,240 (9 KB)Jochen Burghardt (talk | contribs)several possible normalizing paths in canonical rewrite system
20:49, 6 June 2014Thumbnail for version as of 20:49, 6 June 20141,210 × 1,240 (14 KB)Jochen Burghardt (talk | contribs)User created page with UploadWizard

There are no pages that use this file.


Structured data

Items portrayed in this file

no value