diff --git a/build.gradle b/build.gradle
index cc21aa1..1402ea7 100644
--- a/build.gradle
+++ b/build.gradle
@@ -70,7 +70,6 @@ subprojects {
         testCompile group: 'junit', name: 'junit', version: '4.11'
         testCompile group: 'junit', name: 'junit', version: '4.12'
         testCompile('org.mockito:mockito-core:1.10.19') {exclude(group: 'org.hamcrest')}
-
     }
 
     test {
@@ -107,7 +106,11 @@ dependencies {
     compile 'org.slf4j:slf4j-api:1.7.22'
     compile "joda-time:joda-time:2.2"
     compile group: 'org.springframework.boot', name: 'spring-boot-starter-web', version: '2.0.5.RELEASE'
+    compile('org.springframework.boot:spring-boot-starter-web','org.apache.tomcat.embed:tomcat-embed-jasper'
+            ,'javax.servlet:jstl')
 
+    testCompile 'javax.el:javax.el-api:3.0.0'
+    testCompile group: 'org.springframework.boot', name: 'spring-boot-starter-test', version: '2.1.3.RELEASE'
     testCompile group: 'junit', name: 'junit', version: '4.12'
     testCompile "org.springframework:spring-test:5.0.9.RELEASE"
     testCompile('org.mockito:mockito-core:1.10.19') {exclude(group: 'org.hamcrest')}
diff --git a/gradlew~Stashed changes b/gradlew~Stashed changes
deleted file mode 100755
index 4453cce..0000000
--- a/gradlew~Stashed changes	
+++ /dev/null
@@ -1,172 +0,0 @@
-#!/usr/bin/env sh
-
-##############################################################################
-##
-##  Gradle start up script for UN*X
-##
-##############################################################################
-
-# Attempt to set APP_HOME
-# Resolve links: $0 may be a link
-PRG="$0"
-# Need this for relative symlinks.
-while [ -h "$PRG" ] ; do
-    ls=`ls -ld "$PRG"`
-    link=`expr "$ls" : '.*-> \(.*\)$'`
-    if expr "$link" : '/.*' > /dev/null; then
-        PRG="$link"
-    else
-        PRG=`dirname "$PRG"`"/$link"
-    fi
-done
-SAVED="`pwd`"
-cd "`dirname \"$PRG\"`/" >/dev/null
-APP_HOME="`pwd -P`"
-cd "$SAVED" >/dev/null
-
-APP_NAME="Gradle"
-APP_BASE_NAME=`basename "$0"`
-
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS=""
-
-# Use the maximum available, or set MAX_FD != -1 to use that value.
-MAX_FD="maximum"
-
-warn ( ) {
-    echo "$*"
-}
-
-die ( ) {
-    echo
-    echo "$*"
-    echo
-    exit 1
-}
-
-# OS specific support (must be 'true' or 'false').
-cygwin=false
-msys=false
-darwin=false
-nonstop=false
-case "`uname`" in
-  CYGWIN* )
-    cygwin=true
-    ;;
-  Darwin* )
-    darwin=true
-    ;;
-  MINGW* )
-    msys=true
-    ;;
-  NONSTOP* )
-    nonstop=true
-    ;;
-esac
-
-CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar
-
-# Determine the Java command to use to start the JVM.
-if [ -n "$JAVA_HOME" ] ; then
-    if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
-        # IBM's JDK on AIX uses strange locations for the executables
-        JAVACMD="$JAVA_HOME/jre/sh/java"
-    else
-        JAVACMD="$JAVA_HOME/bin/java"
-    fi
-    if [ ! -x "$JAVACMD" ] ; then
-        die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME
-
-Please set the JAVA_HOME variable in your environment to match the
-location of your Java installation."
-    fi
-else
-    JAVACMD="java"
-    which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
-
-Please set the JAVA_HOME variable in your environment to match the
-location of your Java installation."
-fi
-
-# Increase the maximum file descriptors if we can.
-if [ "$cygwin" = "false" -a "$darwin" = "false" -a "$nonstop" = "false" ] ; then
-    MAX_FD_LIMIT=`ulimit -H -n`
-    if [ $? -eq 0 ] ; then
-        if [ "$MAX_FD" = "maximum" -o "$MAX_FD" = "max" ] ; then
-            MAX_FD="$MAX_FD_LIMIT"
-        fi
-        ulimit -n $MAX_FD
-        if [ $? -ne 0 ] ; then
-            warn "Could not set maximum file descriptor limit: $MAX_FD"
-        fi
-    else
-        warn "Could not query maximum file descriptor limit: $MAX_FD_LIMIT"
-    fi
-fi
-
-# For Darwin, add options to specify how the application appears in the dock
-if $darwin; then
-    GRADLE_OPTS="$GRADLE_OPTS \"-Xdock:name=$APP_NAME\" \"-Xdock:icon=$APP_HOME/media/gradle.icns\""
-fi
-
-# For Cygwin, switch paths to Windows format before running java
-if $cygwin ; then
-    APP_HOME=`cygpath --path --mixed "$APP_HOME"`
-    CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
-    JAVACMD=`cygpath --unix "$JAVACMD"`
-
-    # We build the pattern for arguments to be converted via cygpath
-    ROOTDIRSRAW=`find -L / -maxdepth 1 -mindepth 1 -type d 2>/dev/null`
-    SEP=""
-    for dir in $ROOTDIRSRAW ; do
-        ROOTDIRS="$ROOTDIRS$SEP$dir"
-        SEP="|"
-    done
-    OURCYGPATTERN="(^($ROOTDIRS))"
-    # Add a user-defined pattern to the cygpath arguments
-    if [ "$GRADLE_CYGPATTERN" != "" ] ; then
-        OURCYGPATTERN="$OURCYGPATTERN|($GRADLE_CYGPATTERN)"
-    fi
-    # Now convert the arguments - kludge to limit ourselves to /bin/sh
-    i=0
-    for arg in "$@" ; do
-        CHECK=`echo "$arg"|egrep -c "$OURCYGPATTERN" -`
-        CHECK2=`echo "$arg"|egrep -c "^-"`                                 ### Determine if an option
-
-        if [ $CHECK -ne 0 ] && [ $CHECK2 -eq 0 ] ; then                    ### Added a condition
-            eval `echo args$i`=`cygpath --path --ignore --mixed "$arg"`
-        else
-            eval `echo args$i`="\"$arg\""
-        fi
-        i=$((i+1))
-    done
-    case $i in
-        (0) set -- ;;
-        (1) set -- "$args0" ;;
-        (2) set -- "$args0" "$args1" ;;
-        (3) set -- "$args0" "$args1" "$args2" ;;
-        (4) set -- "$args0" "$args1" "$args2" "$args3" ;;
-        (5) set -- "$args0" "$args1" "$args2" "$args3" "$args4" ;;
-        (6) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" ;;
-        (7) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" ;;
-        (8) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" ;;
-        (9) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" "$args8" ;;
-    esac
-fi
-
-# Escape application args
-save ( ) {
-    for i do printf %s\\n "$i" | sed "s/'/'\\\\''/g;1s/^/'/;\$s/\$/' \\\\/" ; done
-    echo " "
-}
-APP_ARGS=$(save "$@")
-
-# Collect all arguments for the java command, following the shell quoting and substitution rules
-eval set -- $DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS "\"-Dorg.gradle.appname=$APP_BASE_NAME\"" -classpath "\"$CLASSPATH\"" org.gradle.wrapper.GradleWrapperMain "$APP_ARGS"
-
-# by default we should be in the correct project dir, but when run from Finder on Mac, the cwd is wrong
-if [ "$(uname)" = "Darwin" ] && [ "$HOME" = "$PWD" ]; then
-  cd "$(dirname "$0")"
-fi
-
-exec "$JAVACMD" "$@"
diff --git a/out/production/classes/META-INF/edu.msudenver.tsp.pandamonium-theorem-prover.main.kotlin_module b/out/production/classes/META-INF/edu.msudenver.tsp.pandamonium-theorem-prover.main.kotlin_module
deleted file mode 100644
index 8fb6019..0000000
Binary files a/out/production/classes/META-INF/edu.msudenver.tsp.pandamonium-theorem-prover.main.kotlin_module and /dev/null differ
diff --git a/out/production/resources/application.properties b/out/production/resources/application.properties
new file mode 100644
index 0000000..f3ce324
--- /dev/null
+++ b/out/production/resources/application.properties
@@ -0,0 +1,2 @@
+spring.mvc.view.prefix:/WEB-INF/jsp/
+spring.mvc.view.suffix:.jsp
\ No newline at end of file
diff --git a/src/main/java/edu/msudenver/tsp/website/Application.java b/src/main/java/edu/msudenver/tsp/website/Application.java
index c8f0854..54da024 100644
--- a/src/main/java/edu/msudenver/tsp/website/Application.java
+++ b/src/main/java/edu/msudenver/tsp/website/Application.java
@@ -1,33 +1,12 @@
 package edu.msudenver.tsp.website;
 
-import lombok.extern.slf4j.Slf4j;
-import org.springframework.boot.CommandLineRunner;
 import org.springframework.boot.SpringApplication;
 import org.springframework.boot.autoconfigure.SpringBootApplication;
-import org.springframework.context.ApplicationContext;
-import org.springframework.context.annotation.Bean;
 
-import java.util.Arrays;
-
-@Slf4j
 @SpringBootApplication
 public class Application {
 
     public static void main(final String[] args) {
         SpringApplication.run(Application.class, args);
     }
-
-    @Bean
-    public CommandLineRunner commandLineRunner(final ApplicationContext ctx) {
-        return args -> {
-
-            LOG.info("Beans provided by Spring Boot:");
-
-            final String[] beanNames = ctx.getBeanDefinitionNames();
-            Arrays.sort(beanNames);
-            for (final String beanName : beanNames) {
-                LOG.info(beanName);
-            }
-        };
-    }
 }
diff --git a/src/main/java/edu/msudenver/tsp/website/ProofsDriver.java b/src/main/java/edu/msudenver/tsp/website/ProofsDriver.java
deleted file mode 100644
index a6d4715..0000000
--- a/src/main/java/edu/msudenver/tsp/website/ProofsDriver.java
+++ /dev/null
@@ -1,4 +0,0 @@
-package edu.msudenver.tsp.website;
-
-public class ProofsDriver {
-}
diff --git a/src/main/java/edu/msudenver/tsp/website/controller/TheoremEntryController.java b/src/main/java/edu/msudenver/tsp/website/controller/TheoremEntryController.java
new file mode 100644
index 0000000..2df1385
--- /dev/null
+++ b/src/main/java/edu/msudenver/tsp/website/controller/TheoremEntryController.java
@@ -0,0 +1,33 @@
+package edu.msudenver.tsp.website.controller;
+
+import edu.msudenver.tsp.website.forms.TheoremForm;
+import lombok.AllArgsConstructor;
+import lombok.extern.slf4j.Slf4j;
+import org.springframework.stereotype.Controller;
+import org.springframework.ui.Model;
+import org.springframework.validation.annotation.Validated;
+import org.springframework.web.bind.annotation.GetMapping;
+import org.springframework.web.bind.annotation.PostMapping;
+import org.springframework.web.bind.annotation.RequestMapping;
+import org.springframework.web.servlet.ModelAndView;
+
+@Slf4j
+@Controller
+@AllArgsConstructor
+@RequestMapping("/theorem")
+public class TheoremEntryController {
+    @GetMapping({"/",""})
+    public ModelAndView enterTheoremPage() {
+        LOG.info("Received request to display the theorem entry page: returning model with name 'Theorem'");
+        return new ModelAndView("Theorem");
+    }
+
+    @PostMapping({"/",""})
+    public String saveTheorem(@Validated final TheoremForm theoremForm, final Model model) {
+        model.addAttribute("theoremName", theoremForm.getTheoremName());
+        model.addAttribute("theorem", theoremForm.getTheorem());
+        LOG.info("Saving theorem {}...", theoremForm);
+
+        return "success";
+    }
+}
\ No newline at end of file
diff --git a/src/main/java/edu/msudenver/tsp/website/forms/TheoremForm.java b/src/main/java/edu/msudenver/tsp/website/forms/TheoremForm.java
new file mode 100644
index 0000000..8cfbd4b
--- /dev/null
+++ b/src/main/java/edu/msudenver/tsp/website/forms/TheoremForm.java
@@ -0,0 +1,11 @@
+package edu.msudenver.tsp.website.forms;
+
+import lombok.Getter;
+import lombok.Setter;
+
+@Getter
+@Setter
+public class TheoremForm {
+    private String theoremName;
+    private String theorem;
+}
diff --git a/src/main/resources/application.properties b/src/main/resources/application.properties
new file mode 100644
index 0000000..a8a0755
--- /dev/null
+++ b/src/main/resources/application.properties
@@ -0,0 +1,3 @@
+spring.mvc.view.prefix:/WEB-INF/jsp/
+spring.mvc.view.suffix:.jsp
+server.port=8090
\ No newline at end of file
diff --git a/src/main/webapp/WEB-INF/jsp/Theorem.jsp b/src/main/webapp/WEB-INF/jsp/Theorem.jsp
new file mode 100644
index 0000000..95826da
--- /dev/null
+++ b/src/main/webapp/WEB-INF/jsp/Theorem.jsp
@@ -0,0 +1,20 @@
+<%@ page contentType="text/html; charset=UTF-8"
+         pageEncoding="UTF-8"%>
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<html>
+    <head>
+        <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+        <title>Theorem Entry</title>
+    </head>
+    <body>
+        <form method="post" action="">
+            <label>Theorem Name:
+                <input type="text" name="theoremName"/>
+            </label>
+            <br><label>Theorem:
+            <input type="text" name="theorem"/>
+        </label><br>
+            <input type="submit" value="Save">
+        </form>
+    </body>
+</html>
\ No newline at end of file
diff --git a/src/main/webapp/WEB-INF/jsp/success.jsp b/src/main/webapp/WEB-INF/jsp/success.jsp
new file mode 100644
index 0000000..4a09232
--- /dev/null
+++ b/src/main/webapp/WEB-INF/jsp/success.jsp
@@ -0,0 +1,7 @@
+<html>
+    <body>
+        <br><b>Name: </b><%= request.getParameter("theoremName")%>
+        <br><b>Theorem: </b><%= request.getParameter("theorem")%>
+
+    </body>
+</html>
\ No newline at end of file
diff --git a/src/test/java/edu/msudenver/tsp/website/ProofsDriverTest.java b/src/test/java/edu/msudenver/tsp/website/ProofsDriverTest.java
deleted file mode 100644
index 04a68e1..0000000
--- a/src/test/java/edu/msudenver/tsp/website/ProofsDriverTest.java
+++ /dev/null
@@ -1,5 +0,0 @@
-package edu.msudenver.tsp.website;
-
-public class ProofsDriverTest {
-
-}
\ No newline at end of file
diff --git a/src/test/java/edu/msudenver/tsp/website/controller/TheoremEntryControllerTest.java b/src/test/java/edu/msudenver/tsp/website/controller/TheoremEntryControllerTest.java
new file mode 100644
index 0000000..2624c17
--- /dev/null
+++ b/src/test/java/edu/msudenver/tsp/website/controller/TheoremEntryControllerTest.java
@@ -0,0 +1,23 @@
+package edu.msudenver.tsp.website.controller;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.mockito.runners.MockitoJUnitRunner;
+import org.springframework.web.servlet.ModelAndView;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertNotNull;
+
+@RunWith(MockitoJUnitRunner.class)
+public class TheoremEntryControllerTest {
+
+    private final TheoremEntryController theoremEntryController = new TheoremEntryController();
+
+    @Test
+    public void testEnterTheoremPage() {
+        final ModelAndView modelAndView = theoremEntryController.enterTheoremPage();
+
+        assertNotNull(modelAndView);
+        assertEquals("Theorem", modelAndView.getViewName());
+    }
+}