initial commit from zip file

HLint.hs

@@ -0,0 +1,4 @@
+import "hint" HLint.Default
+import "hint" HLint.Dollar
+import "hint" HLint.Generalise
+ignore "Use mappend"

README.txt

@@ -0,0 +1,24 @@
+General note
+------------
+
+As described in the accompanying paper, the prover relies heavily on data stored in its _library_.  This library needs to be tailored to the problem(s) being solved. It is not possible to build a general, problem-independent library because the prover will use "more advanced" results to prove simpler ones -- for example, using the fact that a polynomial is differentiable to prove that it is continuous. As such, before trying the prover on fresh problems you will need to update the library. Roughly speaking, the library needs to contain domain-specific results and operations that would be obvious to an undergraduate who could be given the problem as an exercise, without containing "more advanced" facts.  
+
+Compilation and Execution
+-------------------------
+
+This software should be compiled with ghc 7.8.3 and Cabal 1.18.0.5 using v. 0.6.0.2 of the logict package. You will also need a TeX distribution to compile the generated proofs; the software was tested with MikTeX 2.9.
+
+After the source code has been compiled, run run.sh to generate and compile the TeX output; this will generate PDFs in the build/ subdirectory.  robotoneshort.pdf contains the actual proofs 
+
+Changelog
+---------
+
+1.1
+
+Added TestData2 (problems supplied by a referee). 
+forwardsLibraryReasoning no longer creates new terms.
+matchTargetWithHypothesis no longer displays debug text in writeup.
+
+1.0
+
+Initial release.

Setup.lhs

@@ -0,0 +1,6 @@
+#!/usr/bin/runhaskell 
+> module Main where
+> import Distribution.Simple
+> main :: IO ()
+> main = defaultMain
+

count.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+cat src/*.hs | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l

eachcount.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+echo
+pushd src > 0
+for f in *.hs
+do  
+    paste <(cat $f | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l) <(echo ${f%src.*}) 
+done
+echo
+cat *.hs | grep -v -E '^[[:space:]]*($|--( |$)|//)' | wc -l
+popd > 0
+echo

open.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+
+open "$wd/build/robotone.pdf"

out.txt

@@ -0,0 +1,93 @@
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Elementary expansion of hypothesis H3.
+4. Forwards reasoning using H1 with H4.
+5. Deleted H4, as this unexpandable atomic statement is unmatchable.
+6. Deleted H1, as the conclusion of this implicative statement is unmatchable.
+7. Forwards reasoning using H2 with H5.
+8. Deleted H5, as this unexpandable atomic statement is unmatchable.
+9. Deleted H2, as the conclusion of this implicative statement is unmatchable.
+10. Unlock existential-universal-conditional target T3.
+11. Elementary expansion of target T4.
+12. Backwards reasoning using H6 with T5.
+13. Delete H6 as it contans a dangling variable $A$.
+14. Backwards reasoning using H7 with T6.
+15. Delete H7 as it contans a dangling variable $B$.
+16. Replacing diamonds with bullets in L2$^\blacklozenge$.
+17. Backwards reasoning using library result ``transitivity'' with (T7,H8).
+18. Moved H8 down, as $x$ can only be utilised by T8.
+19. Backwards reasoning using library result ``transitivity'' with (T8,H8).
+20. Delete H8 as it contans a dangling variable $x$.
+21. Collapsed subtableau L3 as it has no undeleted hypotheses.
+22. Taking $\delta^\bullet [\overline{y}] = \min(\delta'[x],\delta''[x])$ matches all targets against a library solution, so L2 is done.
+23. All targets of L1 are `Done', so L1 is itself done.
+	23 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Elementary expansion of hypothesis H3.
+4. Forwards reasoning using H2 with H4.
+5. Deleted H4, as this unexpandable atomic statement is unmatchable.
+6. Deleted H2, as the conclusion of this implicative statement is unmatchable.
+7. Unlock existential-universal-conditional target T3.
+8. Elementary expansion of target T4.
+9. Backwards reasoning using H5 with T5.
+10. Delete H5 as it contans a dangling variable $U$.
+11. Backwards reasoning using H1 with T6.
+12. Delete H1 as it contans a dangling variable $f$.
+13. Hypothesis H6 matches target T7 after choosing $\delta^\blacklozenge [\overline{y}] = \delta''[x,\delta'[f(x)]]$, so L2$^\blacklozenge$ is done.
+14. All targets of L1 are `Done', so L1 is itself done.
+	14 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel bare universal target T2.
+3. Unlock existential-universal-conditional target T3.
+4. Backwards reasoning using H2 with T4.
+5. Delete H2 as it contans a dangling variable $g$.
+6. Backwards reasoning using H1 with T5.
+7. Delete H1 as it contans a dangling variable $f$.
+8. Hypothesis H3 matches target T6 after choosing $\delta^\blacklozenge [\overline{y}] = \delta''[x,\delta'[f(x),\epsilon]]$, so L2$^\blacklozenge$ is done.
+9. All targets of L1 are `Done', so L1 is itself done.
+	9 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel bare universal target T2.
+3. Unlock existential-universal-conditional target T3.
+4. Backwards reasoning using H1 with T4.
+5. Delete H1 as it contans a dangling variable $f$.
+6. Backwards reasoning using H2 with T5.
+7. Delete H2 as it contans a dangling variable $a$.
+8. Hypothesis H3 matches target T6 after choosing $N^\blacklozenge [\overline{n}] = N'[\delta[a,\epsilon]]$, so L2$^\blacklozenge$ is done.
+9. All targets of L1 are `Done', so L1 is itself done.
+	9 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Forwards reasoning using H1 with H3.
+4. Deleted H3, as this unexpandable atomic statement is unmatchable.
+5. Deleted H1, as the premise of this implicative statement is unmatchable.
+6. Expand pre-existential hypothesis H5.
+7. Forwards reasoning using library result ``a closed set contains its limit points'' with (H2,H4,H6).
+8. Delete H2 as it contans a dangling variable $X$.
+9. All conjuncts of T3 (after expansion) can be simultaneously matched against H7 and H6 or rendered trivial by choosing $a' = a$, so L1 is done.
+	9 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Expand pre-existential hypothesis H1.
+4. Elementary expansion of hypothesis H2.
+5. Rewrite $x$ as $f(y)$ throughout the tableau using hypothesis H3.
+6. Hypothesis H4 matches target T3, so L1 is done.
+	6 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Elementary expansion of target T3.
+4. All conjuncts of T4 (after expansion) can be simultaneously matched against H1 or rendered trivial by choosing $y = x$, so L1 is done.
+	4 moves made; problem solved.
+1. Expand pre-universal target T1.
+2. Peel and split universal-conditional target T2.
+3. Elementary expansion of hypothesis H2.
+4. Expand pre-existential hypothesis H3.
+5. Expand pre-existential hypothesis H4.
+6. Forwards reasoning using H1 with (H6,H8).
+7. Expand pre-existential target T3.
+8. Unlock existential target T4.
+9. Elementary expansion of target T5.
+10. Rewrite $x$ as $f(y)$ throughout the tableau using hypothesis H6.
+11. Rewrite $y$ as $y'$ throughout the tableau using hypothesis H9.
+	11 moves made.

robotone.cabal

@@ -0,0 +1,28 @@
+name: robotone
+version: 0.0.1
+cabal-version: >=1.2
+build-type: Simple
+license: AllRightsReserved
+license-file: ""
+description:  
+data-dir: ""
+
+executable robotone
+    build-depends: QuickCheck -any, base -any, containers -any,
+                   logict -any, mtl -any, parsec -any, transformers -any
+    main-is: Main.hs
+    buildable: True
+    hs-source-dirs: src
+    other-modules: Writeup Types TidyingMoves TexBase Tex TestData TestData2
+                   Suspension RobotM Rename Printing Parser Move Match Library
+                   Expansion DeletionMoves ApplyingMoves
+    ghc-options: -fwarn-unused-binds
+
+test-suite test-robotone
+    build-depends: QuickCheck -any, base -any, containers -any,
+                   logict -any, mtl -any, parsec -any, transformers -any
+    type: exitcode-stdio-1.0
+    main-is: Main.hs
+    buildable: True
+    cpp-options: -DMAIN_FUNCTION=testMain
+    hs-source-dirs: src

run.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+xelatex=$(which xelatex)
+
+"$wd/dist/build/robotone/robotone" > "$wd/build/robotone.tex"
+echo "TeX"
+pushd "$wd/build"
+"$xelatex" "\input{robotone.tex}" -jobname=robotoneshort -quiet
+"$xelatex" "\def\showsteps{1} \input{robotone.tex}" -jobname=robotone -quiet
+popd

runi.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+xelatex=$(which xelatex)
+
+pushd "$wd/src"
+runghc Main.hs > "../build/robotone.tex"
+popd
+echo "TeX"
+pushd "$wd/build"
+"$xelatex" robotone.tex --quiet
+popd
+open "$wd/build/robotone.pdf"

screen.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/bash
+wd=$(dirname "$0")
+xelatex=$(which xelatex)
+
+"$wd/dist/build/robotone/robotone"