diff --git a/docs/index.html b/docs/index.html
index a0319f0..cd14c67 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -11,6 +11,7 @@
 <link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap-theme.min.css" integrity="sha384-rHyoN1iRsVXV4nD0JutlnGaslCJuC7uwjduW9SVrLvRYooPp2bWYgmgJQIXwl/Sp" crossorigin="anonymous">
 <link rel="stylesheet" href="main.css">
 
+<script defer src="js/i18n.js"></script>
 <script defer src="js/logic.js"></script>
 <script defer src="js/gui.js"></script>
 <script defer src="js/main.js"></script>
diff --git a/docs/js/gui.js b/docs/js/gui.js
index 603b93c..4e5b0cc 100644
--- a/docs/js/gui.js
+++ b/docs/js/gui.js
@@ -1134,7 +1134,7 @@ function deduce(conclusion, justification, law) {
             getElement("proof").hasCircularity = true;
         }
 
-    appendToProof( deductionString("From", justificationSentences, conclusion) + " <I>[" + name + "]</I>");
+    appendToProof( deductionString(qedStr("from"), justificationSentences, conclusion) + " <I>[" + name + "]</I>");
 
 
 
@@ -1645,7 +1645,7 @@ function makeMatches(justification) {
     if (numMatches == 0) {
         var node = document.createElement("LI");
         var span = document.createElement("SPAN");
-        span.innerHTML = "No available deductions can be formed from this selection.";
+        span.innerHTML = qedStr("noDeductions");
         node.appendChild(span);
         proof.appendChild(node);
     }
diff --git a/docs/js/i18n.js b/docs/js/i18n.js
new file mode 100644
index 0000000..9a9dae2
--- /dev/null
+++ b/docs/js/i18n.js
@@ -0,0 +1,55 @@
+"use strict";
+
+var QED_I18N = {
+  en: {
+    deduce: "Deduce",
+    formEnvironment: "Form environment",
+    from: "From",
+    given: "Given",
+    noDeductions: "No available deductions can be formed from this selection.",
+    undo: "IMMEDIATE UNDO",
+    restart: "RESTART EXERCISE",
+    unsolve: "UNSOLVE EXERCISE",
+    prev: "PREVIOUS EXERCISE",
+    next: "NEXT EXERCISE",
+    reset: "RESET QED",
+    editState: "EDIT STATE"
+  }
+};
+
+var QED_LANG = (function () {
+  if (typeof location === "undefined") return "en";
+  var m = /(?:^|[?&])lang=([a-zA-Z-]+)/.exec(location.search);
+  var lang = m ? m[1] : "en";
+  return QED_I18N[lang] ? lang : "en";
+})();
+
+function qedStr(key) {
+  var table = QED_I18N[QED_LANG] || QED_I18N.en;
+  return table[key] || QED_I18N.en[key] || key;
+}
+
+function qedApplyDomStrings() {
+  if (typeof document === "undefined") return;
+  var map = {
+    "undo-button": "undo",
+    "restart-button": "restart",
+    "unsolve-button": "unsolve",
+    "prev-exercise": "prev",
+    "next-exercise": "next",
+    "reset-button": "reset",
+    "edit-state-button": "editState"
+  };
+  Object.keys(map).forEach(function (id) {
+    var el = document.getElementById(id);
+    if (el) el.textContent = qedStr(map[id]);
+  });
+}
+
+if (typeof document !== "undefined") {
+  if (document.readyState === "loading") {
+    document.addEventListener("DOMContentLoaded", qedApplyDomStrings);
+  } else {
+    qedApplyDomStrings();
+  }
+}
diff --git a/docs/js/logic.js b/docs/js/logic.js
index 22b9bfe..ff254ba 100644
--- a/docs/js/logic.js
+++ b/docs/js/logic.js
@@ -41,15 +41,15 @@ function deductionString(prefix, list, conclusion)
 {
  if (list.length == 0) {
     if (conclusion.type == "environment")
-        return "Form environment " + conclusion.name + ".";
+        return qedStr("formEnvironment") + " " + conclusion.name + ".";
     else
-        return "Deduce " + conclusion.name + ".";
+        return qedStr("deduce") + " " + conclusion.name + ".";
  }
  else {
     if (conclusion.type == "environment")
-        return prefix + " " + listToString(list) + ": form environment " + conclusion.name + ".";
+        return prefix + " " + listToString(list) + ": " + qedStr("formEnvironment").toLowerCase() + " " + conclusion.name + ".";
     else
-        return prefix + " " + listToString(list) + ": deduce " + conclusion.name + ".";
+        return prefix + " " + listToString(list) + ": " + qedStr("deduce").toLowerCase() + " " + conclusion.name + ".";
  }
 }
 
@@ -429,7 +429,7 @@ function Law(shortName, name, givens, conclusion) {
     this.givens = givenslist;
     this.conclusion = toContext(conclusion);  // given conclusion
     this.unlocked = false;         // by default the law is not unlocked
-    this.string = deductionString("Given", givens, this.conclusion);
+    this.string = deductionString(qedStr("given"), givens, this.conclusion);
     this.index = allLaws.length;  // the order of the law in the text (used to determine circularity) - the allLaws.length is a placeholder, will be overwritten
     this.clone = "";  // points to the clone of the law with additional root environment, if needed