From d52edc24c1be8eb46c979ffe2dc595ba78e30509 Mon Sep 17 00:00:00 2001
From: Christoph Schwering <c.schwering@unsw.edu.au>
Date: Tue, 14 Feb 2017 22:12:46 +1100
Subject: [PATCH] Renamed minesweeper and textinterface examples; cleaned up.

---
 .gitignore                                    | 18 +++--
 examples/CMakeLists.txt                       |  2 +-
 examples/index.html                           | 79 +++++++++++--------
 examples/jquery.sh                            |  2 +
 examples/minesweeper/CMakeLists.txt           | 18 ++---
 examples/minesweeper/game.h                   | 10 +++
 .../{mw-js.cc => minesweeper-js.cc}           |  0
 .../{mw-js.html => minesweeper-js.html}       | 30 +++----
 .../minesweeper/{mw.cc => minesweeper.cc}     |  0
 examples/minesweeper/test.sh                  |  4 +-
 examples/sudoku/CMakeLists.txt                |  8 +-
 examples/sudoku/sudoku-js.html                | 10 +--
 examples/textinterface/CMakeLists.txt         | 29 -------
 examples/tui/CMakeLists.txt                   | 24 ++++++
 examples/{textinterface => tui}/README.md     |  5 +-
 .../{textinterface => tui}/battleship-pos.hs  |  0
 examples/{textinterface => tui}/battleship.h  |  0
 .../{textinterface => tui}/battleship.txt     |  0
 .../example-battleship-1x4.lela               |  0
 .../example-battleship-4x4.lela               |  0
 examples/tui/example-father-of-sally.lela     | 34 ++++++++
 .../example-father-of-sonny.lela              |  0
 .../example-siblings.lela                     |  0
 .../example-sudoku.lela                       |  0
 .../example-veggie.lela                       |  0
 examples/{textinterface => tui}/sudoku-rep.py |  0
 examples/{textinterface => tui}/sudoku.h      |  0
 .../test-battleship-1x4.lela                  |  0
 .../{textinterface => tui}/test-control.lela  |  0
 .../test-functions.lela                       |  0
 .../test-introspection-constant.lela          |  0
 .../test-introspection-disjunction.lela       |  0
 .../test-introspection-existential.lela       |  0
 .../{textinterface => tui}/test-jesus.lela    |  0
 .../test-propositions.lela                    |  0
 .../{textinterface => tui}/test-siblings.lela |  0
 .../test-veggie-with-guarantee.lela           |  1 +
 .../{textinterface => tui}/test-veggie.lela   |  1 +
 .../{textinterface => tui}/test-ws-1.lela     |  0
 examples/{textinterface => tui}/timer.h       |  0
 .../{textinterface/ti-js.cc => tui/tui-js.cc} |  0
 .../ti-js.html => tui/tui-js.html}            | 37 ++++++---
 examples/{textinterface/ti.cc => tui/tui.cc}  |  0
 examples/upload.sh                            |  2 +
 examples/zip.sh                               | 22 ++++++
 45 files changed, 213 insertions(+), 123 deletions(-)
 create mode 100755 examples/jquery.sh
 rename examples/minesweeper/{mw-js.cc => minesweeper-js.cc} (100%)
 rename examples/minesweeper/{mw-js.html => minesweeper-js.html} (92%)
 rename examples/minesweeper/{mw.cc => minesweeper.cc} (100%)
 delete mode 100644 examples/textinterface/CMakeLists.txt
 create mode 100644 examples/tui/CMakeLists.txt
 rename examples/{textinterface => tui}/README.md (74%)
 rename examples/{textinterface => tui}/battleship-pos.hs (100%)
 rename examples/{textinterface => tui}/battleship.h (100%)
 rename examples/{textinterface => tui}/battleship.txt (100%)
 rename examples/{textinterface => tui}/example-battleship-1x4.lela (100%)
 rename examples/{textinterface => tui}/example-battleship-4x4.lela (100%)
 create mode 100644 examples/tui/example-father-of-sally.lela
 rename examples/{textinterface => tui}/example-father-of-sonny.lela (100%)
 rename examples/{textinterface => tui}/example-siblings.lela (100%)
 rename examples/{textinterface => tui}/example-sudoku.lela (100%)
 rename examples/{textinterface => tui}/example-veggie.lela (100%)
 rename examples/{textinterface => tui}/sudoku-rep.py (100%)
 rename examples/{textinterface => tui}/sudoku.h (100%)
 rename examples/{textinterface => tui}/test-battleship-1x4.lela (100%)
 rename examples/{textinterface => tui}/test-control.lela (100%)
 rename examples/{textinterface => tui}/test-functions.lela (100%)
 rename examples/{textinterface => tui}/test-introspection-constant.lela (100%)
 rename examples/{textinterface => tui}/test-introspection-disjunction.lela (100%)
 rename examples/{textinterface => tui}/test-introspection-existential.lela (100%)
 rename examples/{textinterface => tui}/test-jesus.lela (100%)
 rename examples/{textinterface => tui}/test-propositions.lela (100%)
 rename examples/{textinterface => tui}/test-siblings.lela (100%)
 rename examples/{textinterface => tui}/test-veggie-with-guarantee.lela (97%)
 rename examples/{textinterface => tui}/test-veggie.lela (97%)
 rename examples/{textinterface => tui}/test-ws-1.lela (100%)
 rename examples/{textinterface => tui}/timer.h (100%)
 rename examples/{textinterface/ti-js.cc => tui/tui-js.cc} (100%)
 rename examples/{textinterface/ti-js.html => tui/tui-js.html} (95%)
 rename examples/{textinterface/ti.cc => tui/tui.cc} (100%)
 create mode 100755 examples/upload.sh
 create mode 100755 examples/zip.sh

diff --git a/.gitignore b/.gitignore
index 13dde1e..4b0a746 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,6 +6,12 @@
 
 *.pyc
 
+*.log
+
+callgrind.*
+
+bla*
+
 cpplint.py
 
 CMakeCache.txt
@@ -37,13 +43,13 @@ tests/setup
 tests/solver
 tests/syntax
 tests/term
-examples/minesweeper/mw
-examples/minesweeper/mw-js.js*
-examples/textinterface/ti
-examples/textinterface/ti-js.js*
+examples/minesweeper/minesweeper
+examples/minesweeper/minesweeper-js.js*
+examples/tui/tui
+examples/tui/tui-js.js*
 examples/sudoku/sudoku
 examples/sudoku/sudoku-js.js*
+examples/jquery-*.min.js
 examples/*/jquery-*.min.js
-
-callgrind.*
+examples/demo.*
 
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index ee5d45f..2d9e6a0 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_subdirectory (textinterface)
 add_subdirectory (minesweeper)
 add_subdirectory (sudoku)
+add_subdirectory (tui)
 
diff --git a/examples/index.html b/examples/index.html
index fae68ec..25d6964 100644
--- a/examples/index.html
+++ b/examples/index.html
@@ -4,13 +4,21 @@
     <meta charset="UTF-8"> 
     <title>Limited reasoner demo</title>
 
-    <link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">
+    <!--<link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">-->
     <style type="text/css">
         body { font-family: 'Open Sans', sans-serif; font-size: 140%; }
         p { text-align: justify; }
 
         h1       { font-size: 220%; }
         h2       { font-size: 170%; border-bottom: 1px solid #aaa; }
+
+        ul.demos { font-size: 110%; line-height: 170%; }
+        ul.demos a { font-weight: bold; }
+
+        .logic     { font-family: serif; }
+        .logic b   { font-weight: bold; font-style: normal; }
+        .logic i   { font-weight: normal; font-style: normal; font-size: 75%; line-height: 0; position: relative; vertical-align: baseline; bottom: -0.5ex; }
+        div.logic  { width: 100%; text-align: center; }
     </style>
 </head>
 
@@ -18,8 +26,9 @@
 
 <h1>Limited Reasoner Demos</h1>
 
-<ul style="font-size: 110%; line-height: 170%;">
-    <li> <a href="textinterface/ti-js.html">Text interface</a> demo</li>
+<p>Available demos:</p>
+<ul class="demos">
+    <li> <a href="tui/tui-js.html">Textual user interface</a> demo</li>
     <li> <a href="minesweeper/mw-js.html">Minesweeper</a> demo</li>
     <li> <a href="sudoku/sudoku-js.html">Sudoku</a> demo</li>
 </ul>
@@ -28,51 +37,55 @@
 
 <h2>About the Reasoner</h2>
 
+<h3>Representation</h3>
+
 <p>
-The logical language features functions and equality, first-order quantification, standard names, and sorts.
-(Predicates are not built-in but can be simulated with no overhead using boolean functions.)
-Knowledge bases are restricted to be in clausal form with only universally quantified variables &ndash; these KBs are called proper<sup>+</sup>.
-(Existentially quantified variables in the knowledge base can be simulated with functions.)
-Queries are not subject to any syntactic restriction.
+The reasoner uses a first-order modal logic as representation language.
+In their most basic form, formulas are about the equality of terms&mdash;functions, variables, or standard names.
+For instance, we could say <span class="logic">fatherOf(Sally) = x</span>, where <span class="logic">fatherOf</span> is a unary function, <span class="logic">x</span> is a variable, and <span class="logic">Sally</span> is a standard name (it denotes one specific individual).
+Predicates are not an explicit part of the language, but can be easily simulated with functions and a special standard name <span class="logic">T</span> that indicates truth: <span class="logic">rich(x) = T</span> would represent the <span class="logic">x</span> is in the relation <span class="logic">rich</span>.
+Such literals can be used to form more complex formulas using logical connectives such as logical negation, disjunction/conjunction, and existential/universal quantification.
+For example, <span class="logic">&exist;x (fatherOf(Sally) = x &and; rich(x) = T)</span> means Sally's father is rich.
+Finally, modal operators allow to expressly refer to what is known or considered possible.
+These modal operators are indexed with a natural number that indicates how much reasoning effort is put into proving the formula in its scope.
+A statement such as "I know Sally's father is rich, but I don't know him personally" could be formulised as follows:
 </p>
+<div class="logic"><b>K</b><i>1</i> &exist;x (fatherOf(Sally) = x &and; rich(x) = T &and; <b>M</b><i>1</i> fatherOf(Sally) &ne; x)</div>
 
 <p>
-Decision procedures for sound entailment [KR-2016] and sound consistency [ECAI-2016] are implemented, including conditional beliefs [ECAI-2016] and introspection [IJCAI-2013].
-Adding situation calculus-style actions [KR-2014] is future work.
+The above example is a typical query.
+As for knowledge bases, we make a syntactic restriction to so-called proper<sup>+</sup> formulas: knowledge bases need to be conjunctions of clauses without existential quantifiers.
+Note that every knowledge base can be brought into proper<sup>+</sup> form by converting it into prenex-CNF and Skolemizing the existentialy quantified variables.
+Furthermore, knowledge bases are assumed have no nested modal operators.
 </p>
 
 <p>
-The reasoner is written in C++.
-The code is available at <a href="https://www.github.com/schwering/lela">github.com/schwering/lela</a>.
-This demo is compiled to Javascript by <a href="http://emscripten.org">emscripten</a>.
-As a rule of thumb, the execution time of the Javascript is about 200%&ndash;400% of the comparable native binary on my computer&mdash;this varies however depending on the browser or Javascript engine and the demo.
+To help the reasoner optimise query evaluation, the user provide a guarantee that the knowledge base is consistent with a special modal operator: <span class="logic"><b>G</b> &alpha;</span> indicates that when evaluating <span class="logic">&alpha;</span>, the knowledge base can be assumed to be consistent.
 </p>
 
 <p>
-Please report bugs to <a href="mailto:c.schwering@unsw.edu.au">c.schwering@unsw.edu.au</a>.
+The language furthermore comprises conditional belief to refer to differently plausible beliefs.
+For instance, we could write <span class="logic"><b>B</b> fatherOf(Sally) = Frank &#x27F9; rich(Frank) = T</span> to say that we believe that if Frank is Sally's father, he most presumably is rich.
 </p>
 
+<h3>Reasoning</h3>
 
+<p>
+Reasoning in this language is fundamentally based on case splitting&mdash;that is, by testing all possible denotations of a term like <span class="logic">fatherOf(Sally)</span>&mdash;and on unit propagation and subsumption.
+The reasoning procedures are sound with respect to classical first-order logic, but sacrifice completeness for the sake of decidability.
+This means that whenever <span class="logic"><b>K</b><i>k</i> &alpha;</span> can be inferred from a knowledge base, then <span class="logic"><b>K</b> &alpha;</span> holds in the classical semantics, that is, &alpha; follows from the knowledge base.
+Analogously, whenever <span class="logic"><b>M</b><i>k</i> &alpha;</span> can be inferred from a knowledge base, then <span class="logic"><b>M</b> &alpha;</span> holds in the classical semantics, that is, &alpha; is consistent with the knowledge base.
+</p>
 
-<h2>References</h2>
-<ul>
-    <li>
-        Lakemeyer and Levesque. Decidable Reasoning in a Logic of Limited Belief with Function Symbols. KR 2016.
-        <a href="https://kbsg.rwth-aachen.de/sites/kbsg/files/LakemeyerLevesque2016.pdf">PDF</a></li>
-    <li>
-        Schwering and Lakemeyer. Decidable Reasoning in a First-Order Logic of Limited Conditional Belief. ECAI 2016.
-        <a href="https://kbsg.rwth-aachen.de/sites/kbsg/files/SchweringLakemeyer2016.pdf">PDF</a>
-    </li>
-    <li>
-        Lakemeyer and Levesque. Decidable Reasoning in a Fragment of the Epistemic Situation Calculus. KR 2014.
-        <a href="https://pdfs.semanticscholar.org/8ac9/a2955895cd391ec2b62d8210ee8206979f4a.pdf">PDF</a>
-    </li>
-    <li>
-        Lakemeyer and Levesque. Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals. IJCAI 2013.
-        <a href="https://pdfs.semanticscholar.org/387c/951016c68aaf8ce36bb87e5ea4d1ef42405d.pdf">PDF</a>
-    </li>
-</ul>
+<p>
+The reasoner is implemented in C++ and will be available as open source.
+This demo is compiled to Javascript by <a href="http://emscripten.org">emscripten</a>.
+As a rule of thumb, the execution of the Javascript takes about 200%&ndash;400% of the native binary's execution time&mdash;this may however vary depending on the computer, browser or Javascript engine, and the demo.
+</p>
 
+<p>
+For future work, we plan to integrate sutation calculus-style actions.
+</p>
 
 </body>
 </html>
diff --git a/examples/jquery.sh b/examples/jquery.sh
new file mode 100755
index 0000000..7f78f03
--- /dev/null
+++ b/examples/jquery.sh
@@ -0,0 +1,2 @@
+wget -O "jquery-3.1.1.min.js" "https://code.jquery.com/jquery-3.1.1.min.js"
+
diff --git a/examples/minesweeper/CMakeLists.txt b/examples/minesweeper/CMakeLists.txt
index 90f79d3..30b0ce2 100644
--- a/examples/minesweeper/CMakeLists.txt
+++ b/examples/minesweeper/CMakeLists.txt
@@ -1,26 +1,20 @@
-add_executable (mw mw.cc)
-target_link_libraries (mw LINK_PUBLIC lela)
+add_executable (minesweeper minesweeper.cc)
+target_link_libraries (minesweeper LINK_PUBLIC lela)
 
 set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DUSE_DETERMINES")
 
 find_package (Emscripten)
 if (EMCC)
         if (CMAKE_BUILD_TYPE MATCHES Release)
-                add_custom_command (OUTPUT jquery-3.1.1.min.js
-                        COMMAND wget -O "jquery-3.1.1.min.js" "https://code.jquery.com/jquery-3.1.1.min.js"
-                        DEPENDS jquery-3.1.1.min.js)
-
                 separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
-                add_custom_command (OUTPUT mw-js.js mw-js.js.mem
-                        COMMAND ${EMCC} ${FLAGS} -I../../src mw-js.cc -o mw-js.js
+                add_custom_command (OUTPUT minesweeper-js.js minesweeper-js.js.mem
+                        COMMAND ${EMCC} ${FLAGS} -I../../src minesweeper-js.cc -o minesweeper-js.js
                                 -s EXPORTED_FUNCTIONS=['_lela_init','_lela_play_turn']
                                 -s TOTAL_MEMORY=67108864
                         VERBATIM)
 
-                add_custom_target (mw-js
-                        DEPENDS mw-js.js mw-js.js.mem jquery-3.1.1.min.js)
-
-                add_dependencies (mw mw-js)
+                add_custom_target (minesweeper-js DEPENDS minesweeper-js.js minesweeper-js.js.mem)
+                add_dependencies (minesweeper minesweeper-js)
         endif ()
 endif ()
 
diff --git a/examples/minesweeper/game.h b/examples/minesweeper/game.h
index 047aa91..134d57e 100644
--- a/examples/minesweeper/game.h
+++ b/examples/minesweeper/game.h
@@ -259,6 +259,16 @@ class Game {
     return adjacent_mines;
   }
 
+  int opened_neighbors(Point p) const {
+    int n = 0;
+    for (const Point q : neighbors_of(p)) {
+      if (opened(q)) {
+        ++n;
+      }
+    }
+    return n;
+  }
+
   int unopened_unflagged_neighbors(Point p) const {
     int n = 0;
     for (const Point q : neighbors_of(p)) {
diff --git a/examples/minesweeper/mw-js.cc b/examples/minesweeper/minesweeper-js.cc
similarity index 100%
rename from examples/minesweeper/mw-js.cc
rename to examples/minesweeper/minesweeper-js.cc
diff --git a/examples/minesweeper/mw-js.html b/examples/minesweeper/minesweeper-js.html
similarity index 92%
rename from examples/minesweeper/mw-js.html
rename to examples/minesweeper/minesweeper-js.html
index 54ac9dc..a6c746f 100644
--- a/examples/minesweeper/mw-js.html
+++ b/examples/minesweeper/minesweeper-js.html
@@ -6,7 +6,7 @@
     <meta charset="UTF-8"> 
     <title>Limited reasoner demo</title>
 
-    <!-- <link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet"> -->
+    <!--<link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">-->
     <style type="text/css">
         body { font-family: 'Open Sans', sans-serif; font-size: 140%; }
         p { text-align: justify; }
@@ -37,13 +37,15 @@
         div.table div.row div.cell.new { font-weight: bold; }
         div.table div.row div.cell.flag { background-image: url("flag.svg"); background-size: 60% 80%; background-position: center; background-repeat: no-repeat; }
         div.table div.row div.cell.mine { background-image: url("mine.svg"); background-size: 80% 80%; background-position: center; background-repeat: no-repeat; }
-        div.table div.row div.cell.mistake { background-color: red; font-weight: bold; }
-        div.table div.row div.cell.revealed { background-color: orange; font-weight: bold; }
+        div.table div.row div.cell.mistake { background-color: #ffee00; font-weight: bold; }
+        div.table div.row div.cell.revealed { font-weight: bold; }
+        div.table div.row div.cell.revealed,
         div.table div.row div.cell:empty { background-color: #efefef; }
     </style>
 
-    <script src="jquery-3.1.1.min.js"></script>
-    <script src="mw-js.js"></script>
+    <script src="../jquery-3.1.1.min.js"></script>
+    <script>window.jQuery || document.write('<script src="//ajax.googleapis.com/ajax/libs/jquery/3.1.1/jquery.min.js">\x3C/script>')</script>
+    <script src="minesweeper-js.js"></script>
 </head>
 
 <body>
@@ -93,7 +95,7 @@ $(document).ready(function() {
     $('#scale-field').change(function() { scaleField(); });
     $('#different-seed').click(function() { $('#seed').val(parseInt($('#seed').val()) + 1); scrollToShow('#play-button'); return false; });
     $('#different-field-size').click(function() { scrollToShow('#config-small'); return false; });
-    $('#different-seed-msg').hide();
+    $('#play-again-msg').hide();
     initDisplay();
 });
 
@@ -231,10 +233,10 @@ function updateMessage(arg1, arg2, arg3, arg4) {
     var msg = messages[currentMessage];
     if (gameOver && currentMessage == messages.length - 1) {
         $('#messages').html(msg);
-        $('#different-seed-msg').show();
+        $('#play-again-msg').show();
     } else {
         $('#messages').html(msg);
-        $('#different-seed-msg').hide();
+        $('#play-again-msg').hide();
     }
 }
 
@@ -329,8 +331,8 @@ function showMove(i) {
 }
 
 $(document).ready(function() {
-    $('#field-prev').click(function() { showMove(currentGame - 1); return false; });
-    $('#field-next').click(function() { showMove(currentGame + 1); return false; });
+    $('.field-prev').click(function() { showMove(currentGame - 1); return false; });
+    $('.field-next').click(function() { showMove(currentGame + 1); return false; });
 });
 $(document).keydown(function(e) {
     switch(e.which) {
@@ -348,9 +350,9 @@ $(document).keydown(function(e) {
 
 <p>
 <div id="messages" style="display: inline;">Ready to play!</div>
-<div id="different-seed-msg" style="padding-left: 1ex; display: inline;">
-    To flip through the agent's moves, use the arrow  keys <a href="#field-prev" id="field-prev" style="text-decoration: none;">&#x21e6;</a>  <a href="#field-next" id="field-next" style="text-decoration: none;">&#x21e8;</a>.
-    To play another game, change the <a id="different-seed" href="#">mine placement seed</a> or the <a id="different-field-size" href="#">field size</a>.
+<div id="play-again-msg" style="font-size: 80%; padding-left: 1ex; display: inline;">
+    To flip through the agent's moves, use the arrow  keys <a href="#" class="field-prev" style="text-decoration: none;">&#x21e6;</a>  <a href="#" class="field-next" style="text-decoration: none;">&#x21e8;</a>.
+    To play another round, you could change the <a id="different-seed" href="#">seed</a> or the <a id="different-field-size" href="#">field size</a> to get a new mine placement.
 </div>
 </p>
 
@@ -367,7 +369,7 @@ Known mines are flagged dangerous with a red flag symbol.
 </p>
 
 <p>
-See <a href="#field-prev" id="field-prev">previous</a> / <a href="#field-next" id="field-next">next</a> turn (or use arrow keys &#x21e6; &#x21e8;).
+See <a href="#" class="field-prev">previous</a> / <a href="#" class="field-next">next</a> turn (or use arrow keys <a href="#" class="field-prev" style="text-decoration: none;">&#x21e6;</a> <a href="#" class="field-next" style="text-decoration: none;">&#x21e8;</a>).
 </p>
 
 
diff --git a/examples/minesweeper/mw.cc b/examples/minesweeper/minesweeper.cc
similarity index 100%
rename from examples/minesweeper/mw.cc
rename to examples/minesweeper/minesweeper.cc
diff --git a/examples/minesweeper/test.sh b/examples/minesweeper/test.sh
index a2031f3..123c7f1 100755
--- a/examples/minesweeper/test.sh
+++ b/examples/minesweeper/test.sh
@@ -3,7 +3,7 @@ H=$2
 M=$3
 K=$4
 max=$5
-F=mw-${W}x${H}-${M}-${K}-${max}
-for seed in $(seq 101 $max); do ./mw $W $H $M $seed $K; done | grep '\(Last move\|Exploring\|Flagging\|You\)' >>$F
+F=test-${W}x${H}-${M}-${K}-${max}.log
+for seed in $(seq 101 $max); do ./minesweeper $W $H $M $seed $K; done | grep '\(Last move\|Exploring\|Flagging\|You\)' >>$F
 echo $F
 
diff --git a/examples/sudoku/CMakeLists.txt b/examples/sudoku/CMakeLists.txt
index 3a179b7..2b84b52 100644
--- a/examples/sudoku/CMakeLists.txt
+++ b/examples/sudoku/CMakeLists.txt
@@ -8,10 +8,6 @@ target_link_libraries (sudoku LINK_PUBLIC lela)
 find_package (Emscripten)
 if (EMCC)
         if (CMAKE_BUILD_TYPE MATCHES Release)
-                add_custom_command (OUTPUT jquery-3.1.1.min.js
-                        COMMAND wget -O "jquery-3.1.1.min.js" "https://code.jquery.com/jquery-3.1.1.min.js"
-                        DEPENDS jquery-3.1.1.min.js)
-
                 separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
                 add_custom_command (OUTPUT sudoku-js.js sudoku-js.js.mem
                     COMMAND ${EMCC} ${FLAGS} -I../../src sudoku-js.cc -o sudoku-js.js
@@ -19,9 +15,7 @@ if (EMCC)
                                 -s TOTAL_MEMORY=67108864
                         VERBATIM)
 
-                add_custom_target (sudoku-js
-                        DEPENDS sudoku-js.js sudoku-js.js.mem jquery-3.1.1.min.js)
-
+                add_custom_target (sudoku-js DEPENDS sudoku-js.js sudoku-js.js.mem)
                 add_dependencies (sudoku sudoku-js)
         endif ()
 endif ()
diff --git a/examples/sudoku/sudoku-js.html b/examples/sudoku/sudoku-js.html
index bfeb847..cc0a541 100644
--- a/examples/sudoku/sudoku-js.html
+++ b/examples/sudoku/sudoku-js.html
@@ -6,7 +6,7 @@
     <meta charset="UTF-8"> 
     <title>Limited reasoner demo</title>
 
-    <link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">
+    <!--<link href="https://fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">-->
     <style type="text/css">
         body { font-family: 'Open Sans', sans-serif; font-size: 140%; }
         p { text-align: justify; }
@@ -41,12 +41,8 @@
         #output span.green { color: green; font-weight: bold; }
     </style>
 
-    <script src="jquery-3.1.1.min.js"></script>
-    <script>
-    var Module = {
-        'TOTAL_MEMORY': 128*1024*1024,
-    };
-    </script>
+    <script src="../jquery-3.1.1.min.js"></script>
+    <script>window.jQuery || document.write('<script src="//ajax.googleapis.com/ajax/libs/jquery/3.1.1/jquery.min.js">\x3C/script>')</script>
     <script src="sudoku-js.js"></script>
 </head>
 
diff --git a/examples/textinterface/CMakeLists.txt b/examples/textinterface/CMakeLists.txt
deleted file mode 100644
index 9ca9b4b..0000000
--- a/examples/textinterface/CMakeLists.txt
+++ /dev/null
@@ -1,29 +0,0 @@
-add_executable (ti ti.cc) 
-target_link_libraries (ti LINK_PUBLIC lela)
-
-
-file (GLOB tests RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" "test*.lela")
-foreach (test ${tests})
-    add_test (NAME ${test} COMMAND ./ti ${test})
-endforeach ()
-
-
-find_package (Emscripten)
-if (EMCC)
-        if (CMAKE_BUILD_TYPE MATCHES Release)
-                add_custom_command (OUTPUT jquery-3.1.1.min.js
-                        COMMAND wget -O "jquery-3.1.1.min.js" "https://code.jquery.com/jquery-3.1.1.min.js"
-                        DEPENDS jquery-3.1.1.min.js)
-
-                separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
-                add_custom_command (OUTPUT ti-js.js ti-js.js.mem
-                        COMMAND ${EMCC} ${FLAGS} -I../../src ti-js.cc -o ti-js.js -s EXPORTED_FUNCTIONS=['_lela_parse']
-                        VERBATIM)
-
-                add_custom_target (ti-js
-                        DEPENDS ti-js.js ti-js.js.mem jquery-3.1.1.min.js)
-
-                add_dependencies (ti ti-js)
-        endif ()
-endif ()
-
diff --git a/examples/tui/CMakeLists.txt b/examples/tui/CMakeLists.txt
new file mode 100644
index 0000000..c82e143
--- /dev/null
+++ b/examples/tui/CMakeLists.txt
@@ -0,0 +1,24 @@
+add_executable (tui tui.cc) 
+target_link_libraries (tui LINK_PUBLIC lela)
+
+
+file (GLOB tests RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" "test*.lela")
+foreach (test ${tests})
+    add_test (NAME ${test} COMMAND ./tui ${test})
+endforeach ()
+
+
+find_package (Emscripten)
+if (EMCC)
+        if (CMAKE_BUILD_TYPE MATCHES Release)
+                separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
+                add_custom_command (OUTPUT tui-js.js tui-js.js.mem
+                        COMMAND ${EMCC} ${FLAGS} -I../../src tui-js.cc -o tui-js.js -s EXPORTED_FUNCTIONS=['_lela_parse']
+                                -s TOTAL_MEMORY=16777216
+                        VERBATIM)
+
+                add_custom_target (tui-js DEPENDS tui-js.js tui-js.js.mem)
+                add_dependencies (tui tui-js)
+        endif ()
+endif ()
+
diff --git a/examples/textinterface/README.md b/examples/tui/README.md
similarity index 74%
rename from examples/textinterface/README.md
rename to examples/tui/README.md
index 66d69d1..8b103ab 100644
--- a/examples/textinterface/README.md
+++ b/examples/tui/README.md
@@ -1,4 +1,4 @@
-# Text Interface
+# Terminal
 
 This is a simple text interface to define and query knowledge bases.
 There are two ways to run this demo:
@@ -6,5 +6,6 @@ There are two ways to run this demo:
 * You can run it in your browser:
   <http://www.cse.unsw.edu.au/~cschwering/demo/textinterface/>.
 * You can compile and run it in the terminal; input is read from stdin then:
-  run `cmake ../../ && make` and then run `./ti example-father-of-sonny.txt`.
+  run `cmake ../../ && make` and then
+  run `./terminal example-father-of-sonny.txt`.
 
diff --git a/examples/textinterface/battleship-pos.hs b/examples/tui/battleship-pos.hs
similarity index 100%
rename from examples/textinterface/battleship-pos.hs
rename to examples/tui/battleship-pos.hs
diff --git a/examples/textinterface/battleship.h b/examples/tui/battleship.h
similarity index 100%
rename from examples/textinterface/battleship.h
rename to examples/tui/battleship.h
diff --git a/examples/textinterface/battleship.txt b/examples/tui/battleship.txt
similarity index 100%
rename from examples/textinterface/battleship.txt
rename to examples/tui/battleship.txt
diff --git a/examples/textinterface/example-battleship-1x4.lela b/examples/tui/example-battleship-1x4.lela
similarity index 100%
rename from examples/textinterface/example-battleship-1x4.lela
rename to examples/tui/example-battleship-1x4.lela
diff --git a/examples/textinterface/example-battleship-4x4.lela b/examples/tui/example-battleship-4x4.lela
similarity index 100%
rename from examples/textinterface/example-battleship-4x4.lela
rename to examples/tui/example-battleship-4x4.lela
diff --git a/examples/tui/example-father-of-sally.lela b/examples/tui/example-father-of-sally.lela
new file mode 100644
index 0000000..d1114a6
--- /dev/null
+++ b/examples/tui/example-father-of-sally.lela
@@ -0,0 +1,34 @@
+// Is Sally's father rich?
+
+Sort HUMAN
+Sort BOOL
+
+Variable x -> HUMAN
+Variable y -> HUMAN
+Variable z -> HUMAN
+
+Name Frank -> HUMAN
+Name Fred -> HUMAN
+Name Sally -> HUMAN
+Name T -> BOOL
+
+Function fatherOf/1 -> HUMAN
+Function rich/1 -> BOOL
+
+KB: rich(fatherOf(Sally)) = T
+KB: fatherOf(Sally) = Frank v fatherOf(Sally) = Fred
+
+Assert: K<0> (fatherOf(Sally) = Frank -> rich(Frank) = T)
+Assert: K<0> (fatherOf(Sally) = Fred  -> rich(Fred) = T)
+Refute: K<0> (fatherOf(Sally) = Frank -> rich(Fred) = T)
+Refute: K<0> (rich(Frank) = T v rich(Fred) = T)
+Assert: K<1> (rich(Frank) = T v rich(Fred) = T)
+
+Refute: M<0> (fatherOf(Sally) = Frank)
+Refute: M<0> (fatherOf(Sally) = Fred)
+Assert: M<1> (fatherOf(Sally) = Frank)
+Assert: M<1> (fatherOf(Sally) = Fred)
+Refute: M<0> (rich(Frank) = T)
+Assert: M<1> (rich(Frank) = T)
+Assert: M<1> (rich(Frank) = T)
+
diff --git a/examples/textinterface/example-father-of-sonny.lela b/examples/tui/example-father-of-sonny.lela
similarity index 100%
rename from examples/textinterface/example-father-of-sonny.lela
rename to examples/tui/example-father-of-sonny.lela
diff --git a/examples/textinterface/example-siblings.lela b/examples/tui/example-siblings.lela
similarity index 100%
rename from examples/textinterface/example-siblings.lela
rename to examples/tui/example-siblings.lela
diff --git a/examples/textinterface/example-sudoku.lela b/examples/tui/example-sudoku.lela
similarity index 100%
rename from examples/textinterface/example-sudoku.lela
rename to examples/tui/example-sudoku.lela
diff --git a/examples/textinterface/example-veggie.lela b/examples/tui/example-veggie.lela
similarity index 100%
rename from examples/textinterface/example-veggie.lela
rename to examples/tui/example-veggie.lela
diff --git a/examples/textinterface/sudoku-rep.py b/examples/tui/sudoku-rep.py
similarity index 100%
rename from examples/textinterface/sudoku-rep.py
rename to examples/tui/sudoku-rep.py
diff --git a/examples/textinterface/sudoku.h b/examples/tui/sudoku.h
similarity index 100%
rename from examples/textinterface/sudoku.h
rename to examples/tui/sudoku.h
diff --git a/examples/textinterface/test-battleship-1x4.lela b/examples/tui/test-battleship-1x4.lela
similarity index 100%
rename from examples/textinterface/test-battleship-1x4.lela
rename to examples/tui/test-battleship-1x4.lela
diff --git a/examples/textinterface/test-control.lela b/examples/tui/test-control.lela
similarity index 100%
rename from examples/textinterface/test-control.lela
rename to examples/tui/test-control.lela
diff --git a/examples/textinterface/test-functions.lela b/examples/tui/test-functions.lela
similarity index 100%
rename from examples/textinterface/test-functions.lela
rename to examples/tui/test-functions.lela
diff --git a/examples/textinterface/test-introspection-constant.lela b/examples/tui/test-introspection-constant.lela
similarity index 100%
rename from examples/textinterface/test-introspection-constant.lela
rename to examples/tui/test-introspection-constant.lela
diff --git a/examples/textinterface/test-introspection-disjunction.lela b/examples/tui/test-introspection-disjunction.lela
similarity index 100%
rename from examples/textinterface/test-introspection-disjunction.lela
rename to examples/tui/test-introspection-disjunction.lela
diff --git a/examples/textinterface/test-introspection-existential.lela b/examples/tui/test-introspection-existential.lela
similarity index 100%
rename from examples/textinterface/test-introspection-existential.lela
rename to examples/tui/test-introspection-existential.lela
diff --git a/examples/textinterface/test-jesus.lela b/examples/tui/test-jesus.lela
similarity index 100%
rename from examples/textinterface/test-jesus.lela
rename to examples/tui/test-jesus.lela
diff --git a/examples/textinterface/test-propositions.lela b/examples/tui/test-propositions.lela
similarity index 100%
rename from examples/textinterface/test-propositions.lela
rename to examples/tui/test-propositions.lela
diff --git a/examples/textinterface/test-siblings.lela b/examples/tui/test-siblings.lela
similarity index 100%
rename from examples/textinterface/test-siblings.lela
rename to examples/tui/test-siblings.lela
diff --git a/examples/textinterface/test-veggie-with-guarantee.lela b/examples/tui/test-veggie-with-guarantee.lela
similarity index 97%
rename from examples/textinterface/test-veggie-with-guarantee.lela
rename to examples/tui/test-veggie-with-guarantee.lela
index e364b99..51ebe24 100644
--- a/examples/textinterface/test-veggie-with-guarantee.lela
+++ b/examples/tui/test-veggie-with-guarantee.lela
@@ -1,4 +1,5 @@
 // If she's not Italian, is she a Vegatarian?
+// With consistency guarantee.
 
 Sort FOOD
 Sort BOOL
diff --git a/examples/textinterface/test-veggie.lela b/examples/tui/test-veggie.lela
similarity index 97%
rename from examples/textinterface/test-veggie.lela
rename to examples/tui/test-veggie.lela
index 0e9341f..e38f9dc 100644
--- a/examples/textinterface/test-veggie.lela
+++ b/examples/tui/test-veggie.lela
@@ -1,4 +1,5 @@
 // If she's not Italian, is she a Vegatarian?
+// Without consistency guarantee.
 
 Sort FOOD
 Sort BOOL
diff --git a/examples/textinterface/test-ws-1.lela b/examples/tui/test-ws-1.lela
similarity index 100%
rename from examples/textinterface/test-ws-1.lela
rename to examples/tui/test-ws-1.lela
diff --git a/examples/textinterface/timer.h b/examples/tui/timer.h
similarity index 100%
rename from examples/textinterface/timer.h
rename to examples/tui/timer.h
diff --git a/examples/textinterface/ti-js.cc b/examples/tui/tui-js.cc
similarity index 100%
rename from examples/textinterface/ti-js.cc
rename to examples/tui/tui-js.cc
diff --git a/examples/textinterface/ti-js.html b/examples/tui/tui-js.html
similarity index 95%
rename from examples/textinterface/ti-js.html
rename to examples/tui/tui-js.html
index 47179d7..b9d87e8 100644
--- a/examples/textinterface/ti-js.html
+++ b/examples/tui/tui-js.html
@@ -6,7 +6,7 @@
     <meta charset="UTF-8"> 
     <title>Limited reasoner demo</title>
 
-    <link href="//fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">
+    <!--<link href="//fonts.googleapis.com/css?family=Open+Sans" rel="stylesheet">-->
     <style type="text/css">
         body { font-family: 'Open Sans', sans-serif; font-size: 140%; }
         p { text-align: justify; }
@@ -83,7 +83,8 @@
         .metavariable { font-family: monospace; font-weight: normal; color: #800080; }
     </style>
 
-    <script src="jquery-3.1.1.min.js"></script>
+    <script src="../jquery-3.1.1.min.js"></script>
+    <script>window.jQuery || document.write('<script src="//ajax.googleapis.com/ajax/libs/jquery/3.1.1/jquery.min.js">\x3C/script>')</script>
     <script>
     function getParameterByName(name) {
         var url = window.location.href;
@@ -94,7 +95,18 @@
         if (!results[2]) return '';
         return decodeURIComponent(results[2].replace(/\+/g, " "));
     }
+    </script>
 
+    <script>
+    Module = {
+        'print': function(msg) { printMsg(msg); },
+        'printErr': function(msg) { printDebug(msg); },
+    };
+    </script>
+    <script src="tui-js.js"></script>
+
+    <script>
+    /*
     var Module = null;
 
     function loadEmscripten(mem) {
@@ -110,16 +122,17 @@
             'printErr': function(msg) { printDebug(msg); },
             'TOTAL_MEMORY': mem,
         };
-        src = 'ti-js.js';
+        src = 'tui-js.js';
         $('script[src="' + src + '"]').remove();
         $('<script>').attr('src', src).appendTo('head');
     }
+    */
     </script>
 </head>
 
 <body>
 
-<h1>Limited Reasoner Demo: Text Interface</h1>
+<h1>Limited Reasoner Demo: Textual User Interface</h1>
 
 <p>
 <b>Quick start:</b> have a look at the "Problem Description", hit the "Click me!" button, and check the output under "Reasoning Results".
@@ -134,6 +147,7 @@ For further demos and details on the reasoner, <a href="../">click here</a>.
 <p>
 Load an example:
 <select id="examples">
+<option value="example-father-of-sally">Example: Rich Father</option>
 <option value="example-father-of-sonny">Example: Unknown Father</option>
 <option value="example-siblings">Example: Siblings</option>
 <option value="example-veggie">Example: Veggie</option>
@@ -142,12 +156,15 @@ Load an example:
 <option value="example-battleship-4x4">Example: Battleship 4x4</option>
 <option value="test-propositions">Test: Propositions</option>
 <option value="test-functions">Test: Constants</option>
-<option value="test-introspection">Test: Introspection</option>
-<option value="test-introspection-2">Test: Introspection 2</option>
+<option value="test-introspection-disjunction">Test: Introspection 1</option>
+<option value="test-introspection-existential">Test: Introspection 2</option>
+<option value="test-introspection-constant">Test: Introspection 3</option>
+<option value="test-control">Test: Propositions</option>
 <option value="test-battleship-1x4">Test: Battleship 1x4</option>
 <option value="test-control">Test: Control</option>
 <option value="test-siblings">Test: Siblings</option>
-<option value="test-veggie">Test: Veggie</option>
+<option value="test-veggie">Test: Veggie 1</option>
+<option value="test-veggie-with-guarantee">Test: Veggie 2</option>
 <option value="" style="color: #666;">none</option>
 </select> <br />
 If you like, you can edit the text. For help on the syntax, see <a href="#syntax">below</a>.
@@ -160,9 +177,9 @@ If you like, you can edit the text. For help on the syntax, see <a href="#syntax
 
 <script>
 $(document).ready(function() {
-    loadEmscripten();
+    //loadEmscripten();
     $('#debug-toggle').click(function() { $('#debug-div').toggle(); return false; });
-    $('#enlarge-memory').click(function() { loadEmscripten(128); return false; });
+    //$('#enlarge-memory').click(function() { loadEmscripten(128); return false; });
 
     var select_ex = getParameterByName('ex');
     if (select_ex) {
@@ -297,7 +314,7 @@ Note that the reasoner brings the query formulas into a normal form (similar to
 
 <p>
 <a href="#debug-toggle" id="debug-toggle">Click here</a> to display/hide debug output.
-If more memory is needed (e.g., for some Sudokus), <a href="#enlarge-memory" id="enlarge-memory">click here</a> to enlarge 
+<!--If more memory is needed (e.g., for some Sudokus), <a href="#enlarge-memory" id="enlarge-memory">click here</a> to enlarge.-->
 </p>
 
 
diff --git a/examples/textinterface/ti.cc b/examples/tui/tui.cc
similarity index 100%
rename from examples/textinterface/ti.cc
rename to examples/tui/tui.cc
diff --git a/examples/upload.sh b/examples/upload.sh
new file mode 100755
index 0000000..31a74d4
--- /dev/null
+++ b/examples/upload.sh
@@ -0,0 +1,2 @@
+./zip.sh - | ssh unsw "tar zxvf - -C public_html/demo/"
+
diff --git a/examples/zip.sh b/examples/zip.sh
new file mode 100755
index 0000000..16de77e
--- /dev/null
+++ b/examples/zip.sh
@@ -0,0 +1,22 @@
+OUT=$1
+if [ "$1" == "" ]
+then
+    OUT=demo.zip
+fi
+
+if [[ $OUT == *.zip ]]
+then
+    CMD="zip -r $OUT"
+elif [[ $OUT == *.tar ]]
+then
+    CMD="tar cvf $OUT"
+else
+    CMD="tar zcf $OUT"
+fi
+
+$CMD \
+    index.html jquery*.js \
+    minesweeper/minesweeper-js.{html,js,js.mem} minesweeper/*.svg \
+    sudoku/sudoku-js.{html,js,js.mem} \
+    tui/tui-js.{html,js,js.mem} tui/*.lela
+
-- 
GitLab