+
+Welcome to Narrative AI.
+
+We have a channel on freenode, #narrative-ai, and also a mailing list
+
+
+References
+
+I'll be collecting all the link mentioned on irc or in the Mailing list here:
+
+
+
+
+Authors and Contributors
+
+
+
+
+
+
+
+
+
+
diff --git a/params.json b/params.json
new file mode 100644
index 0000000..a06265a
--- /dev/null
+++ b/params.json
@@ -0,0 +1 @@
+{"name":"Narrative AI","tagline":"Let's recreate Versu's tech as an Open Source framework! And more, ideas welcome. | https://groups.google.com/forum/#!forum/narrative-ai","body":"### Welcome to Narrative AI.\r\nWe have a channel on freenode, #narrative-ai, and also a [mailing list](https://groups.google.com/forum/#!forum/narrative-ai)\r\n\r\n### References\r\nI'll be collecting all the link mentioned on irc or in the [Mailing list](https://groups.google.com/forum/#!forum/narrative-ai) here:\r\n\r\n- [](https://www.cs.cmu.edu/~cmartens/lpnmr13.pdf)\r\n- [Modal Logic for Artificial Intelligence](http://www.phil.uu.nl/~rumberg/infolai/Modal_Logic.pdf)\r\n- [Modal Logic\r\nand Its Applications](https://www.pdx.edu/sites/www.pdx.edu.sysc/files/Perkowski.Seminar.SySc.2011.pdf)\r\n- [Modal Linear Logic in Higher Order Logic - An experiment with COQ](http://eprints.soton.ac.uk/261814/1/tphols03.pdf)\r\n- [Narrative Generators: Sports Games and Story Engines](http://www.gdcvault.com/play/1017987/Narrative-Generators-Sports-Games-and)\r\n- [Versu - AI Game Research](http://www.aigameresearch.org/portfolio-item/versu/)\r\n- [Social Believability in Games Workshops](https://sites.google.com/site/socialbelievabilityingames/home)\r\n- [Epic Mickey's Warren Spector \"Growth of Adult Gaming\" - Full Keynote Speech - D.I.C.E. SUMMIT 2013](https://www.youtube.com/watch?v=v-Fnn0yOw74)\r\n- [Warren Spector On Life After Mickey, Going ‘No Weapons’](http://www.rockpapershotgun.com/2013/05/14/warren-spector-on-life-after-mickey-going-no-weapons/)\r\n\r\n### Authors and Contributors\r\n- @augur\r\n- @meditans\r\n- @doppioslash\r\n- @chrisamaphone","google":"","note":"Don't delete this file! It's used internally to help with page regeneration."}
\ No newline at end of file
diff --git a/stylesheets/github-light.css b/stylesheets/github-light.css
new file mode 100644
index 0000000..872a6f4
--- /dev/null
+++ b/stylesheets/github-light.css
@@ -0,0 +1,116 @@
+/*
+ Copyright 2014 GitHub Inc.
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+
+*/
+
+.pl-c /* comment */ {
+ color: #969896;
+}
+
+.pl-c1 /* constant, markup.raw, meta.diff.header, meta.module-reference, meta.property-name, support, support.constant, support.variable, variable.other.constant */,
+.pl-s .pl-v /* string variable */ {
+ color: #0086b3;
+}
+
+.pl-e /* entity */,
+.pl-en /* entity.name */ {
+ color: #795da3;
+}
+
+.pl-s .pl-s1 /* string source */,
+.pl-smi /* storage.modifier.import, storage.modifier.package, storage.type.java, variable.other, variable.parameter.function */ {
+ color: #333;
+}
+
+.pl-ent /* entity.name.tag */ {
+ color: #63a35c;
+}
+
+.pl-k /* keyword, storage, storage.type */ {
+ color: #a71d5d;
+}
+
+.pl-pds /* punctuation.definition.string, string.regexp.character-class */,
+.pl-s /* string */,
+.pl-s .pl-pse .pl-s1 /* string punctuation.section.embedded source */,
+.pl-sr /* string.regexp */,
+.pl-sr .pl-cce /* string.regexp constant.character.escape */,
+.pl-sr .pl-sra /* string.regexp string.regexp.arbitrary-repitition */,
+.pl-sr .pl-sre /* string.regexp source.ruby.embedded */ {
+ color: #183691;
+}
+
+.pl-v /* variable */ {
+ color: #ed6a43;
+}
+
+.pl-id /* invalid.deprecated */ {
+ color: #b52a1d;
+}
+
+.pl-ii /* invalid.illegal */ {
+ background-color: #b52a1d;
+ color: #f8f8f8;
+}
+
+.pl-sr .pl-cce /* string.regexp constant.character.escape */ {
+ color: #63a35c;
+ font-weight: bold;
+}
+
+.pl-ml /* markup.list */ {
+ color: #693a17;
+}
+
+.pl-mh /* markup.heading */,
+.pl-mh .pl-en /* markup.heading entity.name */,
+.pl-ms /* meta.separator */ {
+ color: #1d3e81;
+ font-weight: bold;
+}
+
+.pl-mq /* markup.quote */ {
+ color: #008080;
+}
+
+.pl-mi /* markup.italic */ {
+ color: #333;
+ font-style: italic;
+}
+
+.pl-mb /* markup.bold */ {
+ color: #333;
+ font-weight: bold;
+}
+
+.pl-md /* markup.deleted, meta.diff.header.from-file */ {
+ background-color: #ffecec;
+ color: #bd2c00;
+}
+
+.pl-mi1 /* markup.inserted, meta.diff.header.to-file */ {
+ background-color: #eaffea;
+ color: #55a532;
+}
+
+.pl-mdr /* meta.diff.range */ {
+ color: #795da3;
+ font-weight: bold;
+}
+
+.pl-mo /* meta.output */ {
+ color: #1d3e81;
+}
+
diff --git a/stylesheets/normalize.css b/stylesheets/normalize.css
new file mode 100644
index 0000000..30366a6
--- /dev/null
+++ b/stylesheets/normalize.css
@@ -0,0 +1,424 @@
+/*! normalize.css v3.0.2 | MIT License | git.io/normalize */
+
+/**
+ * 1. Set default font family to sans-serif.
+ * 2. Prevent iOS text size adjust after orientation change, without disabling
+ * user zoom.
+ */
+
+html {
+ font-family: sans-serif; /* 1 */
+ -ms-text-size-adjust: 100%; /* 2 */
+ -webkit-text-size-adjust: 100%; /* 2 */
+}
+
+/**
+ * Remove default margin.
+ */
+
+body {
+ margin: 0;
+}
+
+/* HTML5 display definitions
+ ========================================================================== */
+
+/**
+ * Correct `block` display not defined for any HTML5 element in IE 8/9.
+ * Correct `block` display not defined for `details` or `summary` in IE 10/11
+ * and Firefox.
+ * Correct `block` display not defined for `main` in IE 11.
+ */
+
+article,
+aside,
+details,
+figcaption,
+figure,
+footer,
+header,
+hgroup,
+main,
+menu,
+nav,
+section,
+summary {
+ display: block;
+}
+
+/**
+ * 1. Correct `inline-block` display not defined in IE 8/9.
+ * 2. Normalize vertical alignment of `progress` in Chrome, Firefox, and Opera.
+ */
+
+audio,
+canvas,
+progress,
+video {
+ display: inline-block; /* 1 */
+ vertical-align: baseline; /* 2 */
+}
+
+/**
+ * Prevent modern browsers from displaying `audio` without controls.
+ * Remove excess height in iOS 5 devices.
+ */
+
+audio:not([controls]) {
+ display: none;
+ height: 0;
+}
+
+/**
+ * Address `[hidden]` styling not present in IE 8/9/10.
+ * Hide the `template` element in IE 8/9/11, Safari, and Firefox < 22.
+ */
+
+[hidden],
+template {
+ display: none;
+}
+
+/* Links
+ ========================================================================== */
+
+/**
+ * Remove the gray background color from active links in IE 10.
+ */
+
+a {
+ background-color: transparent;
+}
+
+/**
+ * Improve readability when focused and also mouse hovered in all browsers.
+ */
+
+a:active,
+a:hover {
+ outline: 0;
+}
+
+/* Text-level semantics
+ ========================================================================== */
+
+/**
+ * Address styling not present in IE 8/9/10/11, Safari, and Chrome.
+ */
+
+abbr[title] {
+ border-bottom: 1px dotted;
+}
+
+/**
+ * Address style set to `bolder` in Firefox 4+, Safari, and Chrome.
+ */
+
+b,
+strong {
+ font-weight: bold;
+}
+
+/**
+ * Address styling not present in Safari and Chrome.
+ */
+
+dfn {
+ font-style: italic;
+}
+
+/**
+ * Address variable `h1` font-size and margin within `section` and `article`
+ * contexts in Firefox 4+, Safari, and Chrome.
+ */
+
+h1 {
+ font-size: 2em;
+ margin: 0.67em 0;
+}
+
+/**
+ * Address styling not present in IE 8/9.
+ */
+
+mark {
+ background: #ff0;
+ color: #000;
+}
+
+/**
+ * Address inconsistent and variable font size in all browsers.
+ */
+
+small {
+ font-size: 80%;
+}
+
+/**
+ * Prevent `sub` and `sup` affecting `line-height` in all browsers.
+ */
+
+sub,
+sup {
+ font-size: 75%;
+ line-height: 0;
+ position: relative;
+ vertical-align: baseline;
+}
+
+sup {
+ top: -0.5em;
+}
+
+sub {
+ bottom: -0.25em;
+}
+
+/* Embedded content
+ ========================================================================== */
+
+/**
+ * Remove border when inside `a` element in IE 8/9/10.
+ */
+
+img {
+ border: 0;
+}
+
+/**
+ * Correct overflow not hidden in IE 9/10/11.
+ */
+
+svg:not(:root) {
+ overflow: hidden;
+}
+
+/* Grouping content
+ ========================================================================== */
+
+/**
+ * Address margin not present in IE 8/9 and Safari.
+ */
+
+figure {
+ margin: 1em 40px;
+}
+
+/**
+ * Address differences between Firefox and other browsers.
+ */
+
+hr {
+ box-sizing: content-box;
+ height: 0;
+}
+
+/**
+ * Contain overflow in all browsers.
+ */
+
+pre {
+ overflow: auto;
+}
+
+/**
+ * Address odd `em`-unit font size rendering in all browsers.
+ */
+
+code,
+kbd,
+pre,
+samp {
+ font-family: monospace, monospace;
+ font-size: 1em;
+}
+
+/* Forms
+ ========================================================================== */
+
+/**
+ * Known limitation: by default, Chrome and Safari on OS X allow very limited
+ * styling of `select`, unless a `border` property is set.
+ */
+
+/**
+ * 1. Correct color not being inherited.
+ * Known issue: affects color of disabled elements.
+ * 2. Correct font properties not being inherited.
+ * 3. Address margins set differently in Firefox 4+, Safari, and Chrome.
+ */
+
+button,
+input,
+optgroup,
+select,
+textarea {
+ color: inherit; /* 1 */
+ font: inherit; /* 2 */
+ margin: 0; /* 3 */
+}
+
+/**
+ * Address `overflow` set to `hidden` in IE 8/9/10/11.
+ */
+
+button {
+ overflow: visible;
+}
+
+/**
+ * Address inconsistent `text-transform` inheritance for `button` and `select`.
+ * All other form control elements do not inherit `text-transform` values.
+ * Correct `button` style inheritance in Firefox, IE 8/9/10/11, and Opera.
+ * Correct `select` style inheritance in Firefox.
+ */
+
+button,
+select {
+ text-transform: none;
+}
+
+/**
+ * 1. Avoid the WebKit bug in Android 4.0.* where (2) destroys native `audio`
+ * and `video` controls.
+ * 2. Correct inability to style clickable `input` types in iOS.
+ * 3. Improve usability and consistency of cursor style between image-type
+ * `input` and others.
+ */
+
+button,
+html input[type="button"], /* 1 */
+input[type="reset"],
+input[type="submit"] {
+ -webkit-appearance: button; /* 2 */
+ cursor: pointer; /* 3 */
+}
+
+/**
+ * Re-set default cursor for disabled elements.
+ */
+
+button[disabled],
+html input[disabled] {
+ cursor: default;
+}
+
+/**
+ * Remove inner padding and border in Firefox 4+.
+ */
+
+button::-moz-focus-inner,
+input::-moz-focus-inner {
+ border: 0;
+ padding: 0;
+}
+
+/**
+ * Address Firefox 4+ setting `line-height` on `input` using `!important` in
+ * the UA stylesheet.
+ */
+
+input {
+ line-height: normal;
+}
+
+/**
+ * It's recommended that you don't attempt to style these elements.
+ * Firefox's implementation doesn't respect box-sizing, padding, or width.
+ *
+ * 1. Address box sizing set to `content-box` in IE 8/9/10.
+ * 2. Remove excess padding in IE 8/9/10.
+ */
+
+input[type="checkbox"],
+input[type="radio"] {
+ box-sizing: border-box; /* 1 */
+ padding: 0; /* 2 */
+}
+
+/**
+ * Fix the cursor style for Chrome's increment/decrement buttons. For certain
+ * `font-size` values of the `input`, it causes the cursor style of the
+ * decrement button to change from `default` to `text`.
+ */
+
+input[type="number"]::-webkit-inner-spin-button,
+input[type="number"]::-webkit-outer-spin-button {
+ height: auto;
+}
+
+/**
+ * 1. Address `appearance` set to `searchfield` in Safari and Chrome.
+ * 2. Address `box-sizing` set to `border-box` in Safari and Chrome
+ * (include `-moz` to future-proof).
+ */
+
+input[type="search"] {
+ -webkit-appearance: textfield; /* 1 */ /* 2 */
+ box-sizing: content-box;
+}
+
+/**
+ * Remove inner padding and search cancel button in Safari and Chrome on OS X.
+ * Safari (but not Chrome) clips the cancel button when the search input has
+ * padding (and `textfield` appearance).
+ */
+
+input[type="search"]::-webkit-search-cancel-button,
+input[type="search"]::-webkit-search-decoration {
+ -webkit-appearance: none;
+}
+
+/**
+ * Define consistent border, margin, and padding.
+ */
+
+fieldset {
+ border: 1px solid #c0c0c0;
+ margin: 0 2px;
+ padding: 0.35em 0.625em 0.75em;
+}
+
+/**
+ * 1. Correct `color` not being inherited in IE 8/9/10/11.
+ * 2. Remove padding so people aren't caught out if they zero out fieldsets.
+ */
+
+legend {
+ border: 0; /* 1 */
+ padding: 0; /* 2 */
+}
+
+/**
+ * Remove default vertical scrollbar in IE 8/9/10/11.
+ */
+
+textarea {
+ overflow: auto;
+}
+
+/**
+ * Don't inherit the `font-weight` (applied by a rule above).
+ * NOTE: the default cannot safely be changed in Chrome and Safari on OS X.
+ */
+
+optgroup {
+ font-weight: bold;
+}
+
+/* Tables
+ ========================================================================== */
+
+/**
+ * Remove most spacing between table cells.
+ */
+
+table {
+ border-collapse: collapse;
+ border-spacing: 0;
+}
+
+td,
+th {
+ padding: 0;
+}
diff --git a/stylesheets/stylesheet.css b/stylesheets/stylesheet.css
new file mode 100644
index 0000000..b5f20c2
--- /dev/null
+++ b/stylesheets/stylesheet.css
@@ -0,0 +1,245 @@
+* {
+ box-sizing: border-box; }
+
+body {
+ padding: 0;
+ margin: 0;
+ font-family: "Open Sans", "Helvetica Neue", Helvetica, Arial, sans-serif;
+ font-size: 16px;
+ line-height: 1.5;
+ color: #606c71; }
+
+a {
+ color: #1e6bb8;
+ text-decoration: none; }
+ a:hover {
+ text-decoration: underline; }
+
+.btn {
+ display: inline-block;
+ margin-bottom: 1rem;
+ color: rgba(255, 255, 255, 0.7);
+ background-color: rgba(255, 255, 255, 0.08);
+ border-color: rgba(255, 255, 255, 0.2);
+ border-style: solid;
+ border-width: 1px;
+ border-radius: 0.3rem;
+ transition: color 0.2s, background-color 0.2s, border-color 0.2s; }
+ .btn + .btn {
+ margin-left: 1rem; }
+
+.btn:hover {
+ color: rgba(255, 255, 255, 0.8);
+ text-decoration: none;
+ background-color: rgba(255, 255, 255, 0.2);
+ border-color: rgba(255, 255, 255, 0.3); }
+
+@media screen and (min-width: 64em) {
+ .btn {
+ padding: 0.75rem 1rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .btn {
+ padding: 0.6rem 0.9rem;
+ font-size: 0.9rem; } }
+
+@media screen and (max-width: 42em) {
+ .btn {
+ display: block;
+ width: 100%;
+ padding: 0.75rem;
+ font-size: 0.9rem; }
+ .btn + .btn {
+ margin-top: 1rem;
+ margin-left: 0; } }
+
+.page-header {
+ color: #fff;
+ text-align: center;
+ background-color: #159957;
+ background-image: linear-gradient(120deg, #155799, #159957); }
+
+@media screen and (min-width: 64em) {
+ .page-header {
+ padding: 5rem 6rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .page-header {
+ padding: 3rem 4rem; } }
+
+@media screen and (max-width: 42em) {
+ .page-header {
+ padding: 2rem 1rem; } }
+
+.project-name {
+ margin-top: 0;
+ margin-bottom: 0.1rem; }
+
+@media screen and (min-width: 64em) {
+ .project-name {
+ font-size: 3.25rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .project-name {
+ font-size: 2.25rem; } }
+
+@media screen and (max-width: 42em) {
+ .project-name {
+ font-size: 1.75rem; } }
+
+.project-tagline {
+ margin-bottom: 2rem;
+ font-weight: normal;
+ opacity: 0.7; }
+
+@media screen and (min-width: 64em) {
+ .project-tagline {
+ font-size: 1.25rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .project-tagline {
+ font-size: 1.15rem; } }
+
+@media screen and (max-width: 42em) {
+ .project-tagline {
+ font-size: 1rem; } }
+
+.main-content :first-child {
+ margin-top: 0; }
+.main-content img {
+ max-width: 100%; }
+.main-content h1, .main-content h2, .main-content h3, .main-content h4, .main-content h5, .main-content h6 {
+ margin-top: 2rem;
+ margin-bottom: 1rem;
+ font-weight: normal;
+ color: #159957; }
+.main-content p {
+ margin-bottom: 1em; }
+.main-content code {
+ padding: 2px 4px;
+ font-family: Consolas, "Liberation Mono", Menlo, Courier, monospace;
+ font-size: 0.9rem;
+ color: #383e41;
+ background-color: #f3f6fa;
+ border-radius: 0.3rem; }
+.main-content pre {
+ padding: 0.8rem;
+ margin-top: 0;
+ margin-bottom: 1rem;
+ font: 1rem Consolas, "Liberation Mono", Menlo, Courier, monospace;
+ color: #567482;
+ word-wrap: normal;
+ background-color: #f3f6fa;
+ border: solid 1px #dce6f0;
+ border-radius: 0.3rem; }
+ .main-content pre > code {
+ padding: 0;
+ margin: 0;
+ font-size: 0.9rem;
+ color: #567482;
+ word-break: normal;
+ white-space: pre;
+ background: transparent;
+ border: 0; }
+.main-content .highlight {
+ margin-bottom: 1rem; }
+ .main-content .highlight pre {
+ margin-bottom: 0;
+ word-break: normal; }
+.main-content .highlight pre, .main-content pre {
+ padding: 0.8rem;
+ overflow: auto;
+ font-size: 0.9rem;
+ line-height: 1.45;
+ border-radius: 0.3rem; }
+.main-content pre code, .main-content pre tt {
+ display: inline;
+ max-width: initial;
+ padding: 0;
+ margin: 0;
+ overflow: initial;
+ line-height: inherit;
+ word-wrap: normal;
+ background-color: transparent;
+ border: 0; }
+ .main-content pre code:before, .main-content pre code:after, .main-content pre tt:before, .main-content pre tt:after {
+ content: normal; }
+.main-content ul, .main-content ol {
+ margin-top: 0; }
+.main-content blockquote {
+ padding: 0 1rem;
+ margin-left: 0;
+ color: #819198;
+ border-left: 0.3rem solid #dce6f0; }
+ .main-content blockquote > :first-child {
+ margin-top: 0; }
+ .main-content blockquote > :last-child {
+ margin-bottom: 0; }
+.main-content table {
+ display: block;
+ width: 100%;
+ overflow: auto;
+ word-break: normal;
+ word-break: keep-all; }
+ .main-content table th {
+ font-weight: bold; }
+ .main-content table th, .main-content table td {
+ padding: 0.5rem 1rem;
+ border: 1px solid #e9ebec; }
+.main-content dl {
+ padding: 0; }
+ .main-content dl dt {
+ padding: 0;
+ margin-top: 1rem;
+ font-size: 1rem;
+ font-weight: bold; }
+ .main-content dl dd {
+ padding: 0;
+ margin-bottom: 1rem; }
+.main-content hr {
+ height: 2px;
+ padding: 0;
+ margin: 1rem 0;
+ background-color: #eff0f1;
+ border: 0; }
+
+@media screen and (min-width: 64em) {
+ .main-content {
+ max-width: 64rem;
+ padding: 2rem 6rem;
+ margin: 0 auto;
+ font-size: 1.1rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .main-content {
+ padding: 2rem 4rem;
+ font-size: 1.1rem; } }
+
+@media screen and (max-width: 42em) {
+ .main-content {
+ padding: 2rem 1rem;
+ font-size: 1rem; } }
+
+.site-footer {
+ padding-top: 2rem;
+ margin-top: 2rem;
+ border-top: solid 1px #eff0f1; }
+
+.site-footer-owner {
+ display: block;
+ font-weight: bold; }
+
+.site-footer-credits {
+ color: #819198; }
+
+@media screen and (min-width: 64em) {
+ .site-footer {
+ font-size: 1rem; } }
+
+@media screen and (min-width: 42em) and (max-width: 64em) {
+ .site-footer {
+ font-size: 1rem; } }
+
+@media screen and (max-width: 42em) {
+ .site-footer {
+ font-size: 0.9rem; } }
diff --git a/subtitles/Pfenning1_0.ass b/subtitles/Pfenning1_0.ass
deleted file mode 100644
index 784b08f..0000000
--- a/subtitles/Pfenning1_0.ass
+++ /dev/null
@@ -1,102 +0,0 @@
-[Script Info]
-; Script generated by Aegisub 3.2.2
-; http://www.aegisub.org/
-Title: Default Aegisub file
-ScriptType: v4.00+
-WrapStyle: 0
-ScaledBorderAndShadow: yes
-YCbCr Matrix: TV.601
-PlayResX: 1440
-PlayResY: 1080
-
-[Aegisub Project Garbage]
-Audio File: ../../../../Downloads/Pfenning1_0.mp4
-Video File: ../../../../Downloads/Pfenning1_0.mp4
-Video AR Mode: 4
-Video AR Value: 1.777778
-Video Zoom Percent: 0.250000
-Scroll Position: 56
-Active Line: 74
-Video Position: 7212
-
-[V4+ Styles]
-Format: Name, Fontname, Fontsize, PrimaryColour, SecondaryColour, OutlineColour, BackColour, Bold, Italic, Underline, StrikeOut, ScaleX, ScaleY, Spacing, Angle, BorderStyle, Outline, Shadow, Alignment, MarginL, MarginR, MarginV, Encoding
-Style: Default,Arial,20,&H00FFFFFF,&H000000FF,&H00000000,&H00000000,0,0,0,0,100,100,0,0,1,2,2,2,10,10,10,1
-
-[Events]
-Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
-Dialogue: 0,0:00:00.98,0:00:03.88,Default,,0,0,0,,So, I'm gonna give a series of 4 lectures
-Dialogue: 0,0:00:06.14,0:00:08.80,Default,,0,0,0,,on Proof Theory and its foundations
-Dialogue: 0,0:00:09.30,0:00:14.22,Default,,0,0,0,,And ... already set me up to some extent in terms of the first lecture.
-Dialogue: 0,0:00:14.66,0:00:18.18,Default,,0,0,0,,you can think of this as being titled Judgements and propositions
-Dialogue: 0,0:00:18.24,0:00:22.36,Default,,0,0,0,,so I will draw the distinction, and talk about
-Dialogue: 0,0:00:22.36,0:00:24.36,Default,,0,0,0,,how we actually define a logic
-Dialogue: 0,0:00:24.36,0:00:25.98,Default,,0,0,0,,what is a logic, how do we define it
-Dialogue: 0,0:00:25.98,0:00:27.06,Default,,0,0,0,,how do we work with it
-Dialogue: 0,0:00:27.36,0:00:29.26,Default,,0,0,0,,and things like that
-Dialogue: 0,0:00:29.26,0:00:32.66,Default,,0,0,0,,and if you think about the trinity picture
-Dialogue: 0,0:00:32.66,0:00:34.40,Default,,0,0,0,,that Bob drew
-Dialogue: 0,0:00:34.42,0:00:38.28,Default,,0,0,0,,so, we had a Proof Theory over here
-Dialogue: 0,0:00:40.78,0:00:44.74,Default,,0,0,0,,and Logic, and here we have Type Theory
-Dialogue: 0,0:00:47.42,0:00:55.56,Default,,0,0,0,,over here, and we had Category Theory over here
-Dialogue: 0,0:00:56.80,0:00:59.22,Default,,0,0,0,,we can also think of this slightly different point of view
-Dialogue: 0,0:00:59.22,0:01:02.86,Default,,0,0,0,,you can think of this as being mostly the domain of Philosophy
-Dialogue: 0,0:01:03.22,0:01:04.82,Default,,0,0,0,,if you will.
-Dialogue: 0,0:01:06.98,0:01:09.52,Default,,0,0,0,,And of course we know how these things are connected.
-Dialogue: 0,0:01:09.52,0:01:12.18,Default,,0,0,0,,and this is Computer Science
-Dialogue: 0,0:01:15.84,0:01:17.78,Default,,0,0,0,,and this is Maths
-Dialogue: 0,0:01:20.92,0:01:24.00,Default,,0,0,0,,and one of the reasons why we're doing this kind of thing
-Dialogue: 0,0:01:24.00,0:01:26.78,Default,,0,0,0,,together is to show that they're all aspects of
-Dialogue: 0,0:01:26.78,0:01:28.78,Default,,0,0,0,,the same thing that we're trying to do.
-Dialogue: 0,0:01:29.54,0:01:32.66,Default,,0,0,0,,Today in the first lecture I'll stay mostly in this
-Dialogue: 0,0:01:32.66,0:01:35.36,Default,,0,0,0,,in this realm here, Philosophy, Logic and Proof Theory
-Dialogue: 0,0:01:35.36,0:01:39.72,Default,,0,0,0,,even though I'll make some brief connections to the other topics.
-Dialogue: 0,0:01:40.44,0:01:42.82,Default,,0,0,0,,and then, in the second lecture
-Dialogue: 0,0:01:43.74,0:01:46.68,Default,,0,0,0,,I'll taks about Proofs as programs
-Dialogue: 0,0:01:51.70,0:01:55.54,Default,,0,0,0,,I reserve the right to adjust this lecture, as I see what Bob's actually doing
-Dialogue: 0,0:01:57.30,0:02:00.58,Default,,0,0,0,,I'm gonna try to move a bit into this direction
-Dialogue: 0,0:02:00.58,0:02:03.80,Default,,0,0,0,,ok, so away from this, into this direction
-Dialogue: 0,0:02:05.36,0:02:08.22,Default,,0,0,0,,in the third one I'll talk about Proof search
-Dialogue: 0,0:02:12.40,0:02:14.60,Default,,0,0,0,,this is a very important topic
-Dialogue: 0,0:02:14.60,0:02:18.92,Default,,0,0,0,,perhaps not so much because, I mean there is a connection, of course
-Dialogue: 0,0:02:18.92,0:02:20.92,Default,,0,0,0,,in this picture
-Dialogue: 0,0:02:20.92,0:02:24.60,Default,,0,0,0,,on this side, we can ??? Sequent Calculus
-Dialogue: 0,0:02:26.30,0:02:31.04,Default,,0,0,0,,but also, if you use a sistem like Coq
-Dialogue: 0,0:02:32.04,0:02:33.78,Default,,0,0,0,,then you're doing Theorem Proving
-Dialogue: 0,0:02:33.78,0:02:35.92,Default,,0,0,0,,and when you're doing Theorem Proving you need to understand
-Dialogue: 0,0:02:35.92,0:02:37.92,Default,,0,0,0,,how you search for proofs
-Dialogue: 0,0:02:37.92,0:02:39.96,Default,,0,0,0,,and so it's very important to talk about the
-Dialogue: 0,0:02:39.96,0:02:43.30,Default,,0,0,0,,basic principles of Proof search you can use this kind of things effectively
-Dialogue: 0,0:02:43.30,0:02:45.30,Default,,0,0,0,,so that's the third lecture
-Dialogue: 0,0:02:45.86,0:02:47.38,Default,,0,0,0,,and I'm kind of still edging my bets
-Dialogue: 0,0:02:47.38,0:02:49.38,Default,,0,0,0,,on the fourth lecture, to see
-Dialogue: 0,0:02:49.38,0:02:51.38,Default,,0,0,0,,exactly what I'm gonna do. What I did last year was
-Dialogue: 0,0:02:51.38,0:02:53.38,Default,,0,0,0,,called focusing, and I might do that again
-Dialogue: 0,0:02:53.38,0:02:56.34,Default,,0,0,0,,or I might brach out in some different direction, talk about
-Dialogue: 0,0:02:56.34,0:02:58.34,Default,,0,0,0,,some other topic, like Monads
-Dialogue: 0,0:02:58.34,0:03:00.34,Default,,0,0,0,,and things like that
-Dialogue: 0,0:03:02.06,0:03:03.84,Default,,0,0,0,,let's come to the first topic
-Dialogue: 0,0:03:03.84,0:03:05.84,Default,,0,0,0,,Judgements and propositions
-Dialogue: 0,0:03:12.72,0:03:15.52,Default,,0,0,0,,what I've already ??? the basic idea
-Dialogue: 0,0:03:15.52,0:03:19.90,Default,,0,0,0,,that we have when we make a judgement, something like "a is true"
-Dialogue: 0,0:03:21.12,0:03:24.32,Default,,0,0,0,,and this thing here is a proposition
-Dialogue: 0,0:03:27.86,0:03:31.02,Default,,0,0,0,,and the thing taken as a whole, that's what we call a Judgement
-Dialogue: 0,0:03:34.40,0:03:38.06,Default,,0,0,0,,And Martin Lof would say that a judgement is an object of knowledge
-Dialogue: 0,0:03:38.06,0:03:40.06,Default,,0,0,0,,it is something that we actually know
-Dialogue: 0,0:03:40.06,0:03:42.76,Default,,0,0,0,,where a proposition is something in particular
-Dialogue: 0,0:03:42.76,0:03:44.76,Default,,0,0,0,,about which we make ??? different judgements
-Dialogue: 0,0:03:45.44,0:03:52.26,Default,,0,0,0,,and so we can think of other judgements to make about propositions, besides the fact that they're true
-Dialogue: 0,0:03:54.42,0:03:57.40,Default,,0,0,0,,so another judgement I want to make, for example is to say
-Dialogue: 0,0:03:58.20,0:04:00.64,Default,,0,0,0,,it is false
-Dialogue: 0,0:04:00.64,0:04:02.64,Default,,0,0,0,,that a typical judgement that we often make
-Dialogue: 0,0:04:02.64,0:04:04.64,Default,,0,0,0,,about a proposition
-Dialogue: 0,0:04:04.64,0:04:06.64,Default,,0,0,0,,another judgement you this morning
-Dialogue: 0,0:04:06.64,0:04:08.16,Default,,0,0,0,,which is
-Dialogue: 0,0:04:08.16,0:04:10.16,Default,,0,0,0,,? is a proof of a or
-Dialogue: 0,0:04:10.16,0:04:12.16,Default,,0,0,0,,equivalent to say that M is
-Dialogue: 0,0:04:12.16,0:04:14.16,Default,,0,0,0,,a program which has type A
-Dialogue: 0,0:04:15.10,0:04:17.72,Default,,0,0,0,,so we know that, by the connection between
-Dialogue: 0,0:04:17.72,0:04:21.08,Default,,0,0,0,,two pause on this triangle there
-Dialogue: 0,0:04:21.08,0:04:23.08,Default,,0,0,0,,that these are really the same thing
-Dialogue: 0,0:04:23.08,0:04:25.08,Default,,0,0,0,,it's another judgement
-Dialogue: 0,0:04:25.08,0:04:27.08,Default,,0,0,0,,