summaryrefslogtreecommitdiff
path: root/prolog
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-12-10 17:19:36 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-12-10 17:19:36 +0100
commitfc4ba27f71e8a806d95fb441c1ee2e8e065b48fe (patch)
tree992f1f1f1ec8bb197f38d337bf8e7cee8970d7a4 /prolog
parente88fae1aa94743b0596a60b9ff3798753c1027c0 (diff)
downloadlambda-nantes-fc4ba27f71e8a806d95fb441c1ee2e8e065b48fe.tar.gz
Add basic readme for Prolog workshop
Diffstat (limited to 'prolog')
-rw-r--r--prolog/README.html453
-rw-r--r--prolog/README.md148
-rw-r--r--prolog/star-wars.jpgbin0 -> 530628 bytes
-rw-r--r--prolog/workbench.jpgbin0 -> 1815874 bytes
4 files changed, 590 insertions, 11 deletions
diff --git a/prolog/README.html b/prolog/README.html
new file mode 100644
index 0000000..e521647
--- /dev/null
+++ b/prolog/README.html
@@ -0,0 +1,453 @@
+<!DOCTYPE html>
+<html>
+<head>
+ <meta charset="utf-8">
+ <meta name="generator" content="pandoc">
+ <meta name="author" content="arnaud@pankzsoft.com - @abailly.bsky.social">
+ <meta name="dcterms.date" content="2025-12-10">
+ <title>Implementing Prolog</title>
+ <meta name="apple-mobile-web-app-capable" content="yes">
+ <meta name="apple-mobile-web-app-status-bar-style" content="black-translucent">
+ <meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no, minimal-ui">
+ <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reset.css">
+ <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reveal.css">
+ <style>
+ .reveal .sourceCode { /* see #7635 */
+ overflow: visible;
+ }
+ /* Default styles provided by pandoc.
+ ** See https://pandoc.org/MANUAL.html#variables-for-html for config info.
+ */
+ code{white-space: pre-wrap;}
+ span.smallcaps{font-variant: small-caps;}
+ div.columns{display: flex; gap: min(4vw, 1.5em);}
+ div.column{flex: auto; overflow-x: auto;}
+ div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
+ /* The extra [class] is a hack that increases specificity enough to
+ override a similar rule in reveal.js */
+ ul.task-list[class]{list-style: none;}
+ ul.task-list li input[type="checkbox"] {
+ font-size: inherit;
+ width: 0.8em;
+ margin: 0 0.8em 0.2em -1.6em;
+ vertical-align: middle;
+ }
+ .display.math{display: block; text-align: center; margin: 0.5rem auto;}
+ /* CSS for syntax highlighting */
+ html { -webkit-text-size-adjust: 100%; }
+ pre > code.sourceCode { white-space: pre; position: relative; }
+ pre > code.sourceCode > span { display: inline-block; line-height: 1.25; }
+ pre > code.sourceCode > span:empty { height: 1.2em; }
+ .sourceCode { overflow: visible; }
+ code.sourceCode > span { color: inherit; text-decoration: inherit; }
+ div.sourceCode { margin: 1em 0; }
+ pre.sourceCode { margin: 0; }
+ @media screen {
+ div.sourceCode { overflow: auto; }
+ }
+ @media print {
+ pre > code.sourceCode { white-space: pre-wrap; }
+ pre > code.sourceCode > span { text-indent: -5em; padding-left: 5em; }
+ }
+ pre.numberSource code
+ { counter-reset: source-line 0; }
+ pre.numberSource code > span
+ { position: relative; left: -4em; counter-increment: source-line; }
+ pre.numberSource code > span > a:first-child::before
+ { content: counter(source-line);
+ position: relative; left: -1em; text-align: right; vertical-align: baseline;
+ border: none; display: inline-block;
+ -webkit-touch-callout: none; -webkit-user-select: none;
+ -khtml-user-select: none; -moz-user-select: none;
+ -ms-user-select: none; user-select: none;
+ padding: 0 4px; width: 4em;
+ }
+ pre.numberSource { margin-left: 3em; padding-left: 4px; }
+ div.sourceCode
+ { color: #cccccc; background-color: #303030; }
+ @media screen {
+ pre > code.sourceCode > span > a:first-child::before { text-decoration: underline; }
+ }
+ code span.al { color: #ffcfaf; } /* Alert */
+ code span.an { color: #7f9f7f; font-weight: bold; } /* Annotation */
+ code span.at { } /* Attribute */
+ code span.bn { color: #dca3a3; } /* BaseN */
+ code span.bu { } /* BuiltIn */
+ code span.cf { color: #f0dfaf; } /* ControlFlow */
+ code span.ch { color: #dca3a3; } /* Char */
+ code span.cn { color: #dca3a3; font-weight: bold; } /* Constant */
+ code span.co { color: #7f9f7f; } /* Comment */
+ code span.cv { color: #7f9f7f; font-weight: bold; } /* CommentVar */
+ code span.do { color: #7f9f7f; } /* Documentation */
+ code span.dt { color: #dfdfbf; } /* DataType */
+ code span.dv { color: #dcdccc; } /* DecVal */
+ code span.er { color: #c3bf9f; } /* Error */
+ code span.ex { } /* Extension */
+ code span.fl { color: #c0bed1; } /* Float */
+ code span.fu { color: #efef8f; } /* Function */
+ code span.im { } /* Import */
+ code span.in { color: #7f9f7f; font-weight: bold; } /* Information */
+ code span.kw { color: #f0dfaf; } /* Keyword */
+ code span.op { color: #f0efd0; } /* Operator */
+ code span.ot { color: #efef8f; } /* Other */
+ code span.pp { color: #ffcfaf; font-weight: bold; } /* Preprocessor */
+ code span.sc { color: #dca3a3; } /* SpecialChar */
+ code span.ss { color: #cc9393; } /* SpecialString */
+ code span.st { color: #cc9393; } /* String */
+ code span.va { } /* Variable */
+ code span.vs { color: #cc9393; } /* VerbatimString */
+ code span.wa { color: #7f9f7f; font-weight: bold; } /* Warning */
+ </style>
+ <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/theme/black.css" id="theme">
+</head>
+<body>
+ <div class="reveal">
+ <div class="slides">
+
+<section id="title-slide">
+ <h1 class="title">Implementing Prolog</h1>
+ <p class="subtitle">A λ-Nantes Workshop</p>
+ <p class="author">arnaud@pankzsoft.com - <span class="citation"
+data-cites="abailly.bsky.social">@abailly.bsky.social</span></p>
+ <p class="date">2025-12-10</p>
+</section>
+
+<section>
+<section id="usage" class="title-slide slide level1">
+<h1>Usage</h1>
+<p><img data-src="star-wars.jpg" /></p>
+</section>
+<section id="example" class="slide level2">
+<h2>Example</h2>
+<p>A <em>program</em> about Star Wars characters (including the crappy
+recent ones)</p>
+</section>
+<section id="example---facts" class="slide level2">
+<h2>Example - Facts</h2>
+<p>Simple facts asserting the gender of some characters.</p>
+<div class="sourceCode" id="cb1"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb1-1"><a href="#cb1-1" aria-hidden="true" tabindex="-1"></a>female(leia)<span class="kw">.</span></span>
+<span id="cb1-2"><a href="#cb1-2" aria-hidden="true" tabindex="-1"></a>male(vader)<span class="kw">.</span></span>
+<span id="cb1-3"><a href="#cb1-3" aria-hidden="true" tabindex="-1"></a>male(luke)<span class="kw">.</span></span>
+<span id="cb1-4"><a href="#cb1-4" aria-hidden="true" tabindex="-1"></a>male(kylo)<span class="kw">.</span></span></code></pre></div>
+</section>
+<section id="example---facts-1" class="slide level2">
+<h2>Example - Facts</h2>
+<p>More complex facts asserting a <code>child</code>hood
+<em>relation</em> between some characters.</p>
+<div class="sourceCode" id="cb2"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb2-1"><a href="#cb2-1" aria-hidden="true" tabindex="-1"></a>child(luke<span class="kw">,</span> vader)<span class="kw">.</span></span>
+<span id="cb2-2"><a href="#cb2-2" aria-hidden="true" tabindex="-1"></a>child(leia<span class="kw">,</span> vader)<span class="kw">.</span></span>
+<span id="cb2-3"><a href="#cb2-3" aria-hidden="true" tabindex="-1"></a>child(kylo<span class="kw">,</span> leia)<span class="kw">.</span></span></code></pre></div>
+</section>
+<section id="example---rules" class="slide level2">
+<h2>Example - Rules</h2>
+<p><em>Rules</em> (or <em>Clauses</em>) allowing to infer some relation
+from other relations.</p>
+<div class="sourceCode" id="cb3"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb3-1"><a href="#cb3-1" aria-hidden="true" tabindex="-1"></a>son(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>) <span class="kw">:-</span> male(<span class="dt">X</span>)<span class="kw">,</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">.</span></span>
+<span id="cb3-2"><a href="#cb3-2" aria-hidden="true" tabindex="-1"></a>daughter(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>) <span class="kw">:-</span> female(<span class="dt">X</span>)<span class="kw">,</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">.</span></span></code></pre></div>
+</section>
+<section id="example---rules-1" class="slide level2">
+<h2>Example - Rules</h2>
+<p>More complex rules asserting a transitive relation</p>
+<div class="sourceCode" id="cb4"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb4-1"><a href="#cb4-1" aria-hidden="true" tabindex="-1"></a>grandchild(<span class="dt">X</span><span class="kw">,</span><span class="dt">Z</span>) <span class="kw">:-</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">,</span> child(<span class="dt">Y</span><span class="kw">,</span><span class="dt">Z</span>)<span class="kw">.</span></span></code></pre></div>
+</section>
+<section id="example---query" class="slide level2">
+<h2>Example - Query</h2>
+<p>We can <em>query</em> this program, for example asking who is a
+grandchild of Darth Vader</p>
+<div class="sourceCode" id="cb5"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb5-1"><a href="#cb5-1" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span> <span class="fu">?-</span> grandchild(<span class="dt">X</span><span class="er">,</span> vader)<span class="kw">.</span></span>
+<span id="cb5-2"><a href="#cb5-2" aria-hidden="true" tabindex="-1"></a>success<span class="kw">.</span> <span class="dt">Type</span> [<span class="dt">Enter</span>] to list solutions<span class="kw">.</span></span>
+<span id="cb5-3"><a href="#cb5-3" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span></span>
+<span id="cb5-4"><a href="#cb5-4" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-&gt;</span> kylo<span class="er">]</span></span></code></pre></div>
+</section>
+<section id="example---query-1" class="slide level2">
+<h2>Example - Query</h2>
+<p>A Prolog query can have several answers:</p>
+<div class="sourceCode" id="cb6"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb6-1"><a href="#cb6-1" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span> <span class="fu">?-</span> child(<span class="dt">X</span><span class="er">,</span> vader)<span class="kw">.</span></span>
+<span id="cb6-2"><a href="#cb6-2" aria-hidden="true" tabindex="-1"></a>success<span class="kw">.</span> <span class="dt">Type</span> [<span class="dt">Enter</span>] to list solutions<span class="kw">.</span></span>
+<span id="cb6-3"><a href="#cb6-3" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span></span>
+<span id="cb6-4"><a href="#cb6-4" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-&gt;</span> luke<span class="er">]</span></span>
+<span id="cb6-5"><a href="#cb6-5" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span></span>
+<span id="cb6-6"><a href="#cb6-6" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-&gt;</span> leia<span class="er">]</span></span></code></pre></div>
+</section>
+<section id="example---query-2" class="slide level2">
+<h2>Example - Query</h2>
+<p>Or no answer:</p>
+<div class="sourceCode" id="cb7"><pre
+class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb7-1"><a href="#cb7-1" aria-hidden="true" tabindex="-1"></a><span class="dt">&gt;</span> <span class="fu">?-</span> grandchild(leia<span class="er">,</span> <span class="dt">X</span>)<span class="kw">.</span></span>
+<span id="cb7-2"><a href="#cb7-2" aria-hidden="true" tabindex="-1"></a>failure</span></code></pre></div>
+</section></section>
+<section>
+<section id="implementation" class="title-slide slide level1">
+<h1>Implementation</h1>
+
+</section>
+<section id="terms" class="slide level2">
+<h2>Terms</h2>
+<ul>
+<li class="fragment">variables start with upper casae: <code>X</code>,
+<code>Y</code>…</li>
+<li class="fragment">symbols start with lower case: <code>s</code>,
+<code>z</code>, <code>child</code>, …</li>
+<li class="fragment">symbols have 0 or more arguments, e.g an
+<em>arity</em> : <code>bob</code>, <code>child(X, Y)</code>,
+<code>father(bob, Z)</code>…</li>
+</ul>
+</section>
+<section id="clauses" class="slide level2">
+<h2>Clauses</h2>
+<ul>
+<li class="fragment"><em>head</em>: a single term</li>
+<li class="fragment"><em>premises</em>: a (possibly empty) list of
+terms</li>
+<li class="fragment">a <em>data set</em> (or a <em>program</em>) is a
+list of clauses or <em>facts</em></li>
+<li class="fragment">a <em>query</em> is a term introduced with
+<code>?-</code></li>
+</ul>
+</section>
+<section id="basic-algorithm" class="slide level2">
+<h2>Basic algorithm</h2>
+<p>Given a query and a set of clauses, a Prolog interpreter loop goes
+like:</p>
+<ol type="1">
+<li class="fragment">Push <em>query</em> on its goal stack</li>
+<li class="fragment">Pop up current <em>goal</em> from the stack</li>
+<li class="fragment">Try to match <em>goal</em> with each
+<em>clause</em>:
+<ol type="a">
+<li class="fragment"><em>Unify</em> goal with the <em>head</em> of
+<em>clause</em> with <em>fresh</em> variables</li>
+<li class="fragment">If unification succeeds, push <em>premises</em> of
+clause onto goals stack</li>
+</ol></li>
+<li class="fragment">Query succeeds if stack is empty with a successful
+match</li>
+</ol>
+</section>
+<section id="unification" class="slide level2">
+<h2>Unification</h2>
+<p>Given two terms <span
+class="math inline"><em>t</em><sub>1</sub></span> and <span
+class="math inline"><em>t</em><sub>2</sub></span> with <em>free
+variables</em> <span
+class="math inline"><em>f</em><em>v</em>(<em>t</em><sub>1</sub>)</span>,
+<span
+class="math inline"><em>f</em><em>v</em>(<em>t</em><sub>2</sub>)</span>,
+unification is the process of defining a <em>substitution</em> between
+variables and <em>terms</em></p>
+<p><span
+class="math display"><em>σ</em> : <em>f</em><em>v</em>(<em>t</em><sub>1</sub>) ∪ <em>f</em><em>v</em>(<em>t</em><sub>2</sub>) → <em>T</em></span></p>
+</section>
+<section id="unification-1" class="slide level2">
+<h2>Unification</h2>
+<ul>
+<li class="fragment">Two variables unify with each other</li>
+<li class="fragment">A variable unifies with a term if not already
+mapped</li>
+<li class="fragment">Two relations unify with each other iff
+<ul>
+<li class="fragment">Their symbol is the same</li>
+<li class="fragment">Their arguments unify with each other</li>
+</ul></li>
+</ul>
+</section>
+<section id="unification-2" class="slide level2">
+<h2>Unification</h2>
+<ul>
+<li class="fragment"><span
+class="math inline"><em>σ</em>(<em>X</em>, <em>Y</em>) = {<em>X</em> ↦ <em>Y</em>}</span></li>
+<li class="fragment"><span
+class="math inline"><em>σ</em>(<em>X</em>, <em>f</em><em>o</em><em>o</em>) = {<em>X</em> ↦ <em>f</em><em>o</em><em>o</em>}</span></li>
+<li class="fragment"><span
+class="math inline"><em>σ</em>(<em>f</em><em>o</em><em>o</em>, <em>X</em>) = {<em>X</em> ↦ <em>f</em><em>o</em><em>o</em>}</span></li>
+<li class="fragment"><span
+class="math inline"><em>σ</em>(<em>f</em><em>o</em><em>o</em>(<em>b</em><em>a</em><em>r</em>, <em>Y</em>), <em>f</em><em>o</em><em>o</em>(<em>X</em>, <em>Z</em>)) = {<em>X</em> ↦ <em>b</em><em>a</em><em>r</em>, <em>Y</em> ↦ <em>Z</em>}</span></li>
+</ul>
+</section></section>
+<section>
+<section id="practice" class="title-slide slide level1">
+<h1>Practice</h1>
+<p><img data-src="workbench.jpg" /></p>
+</section>
+<section id="references" class="slide level2">
+<h2>References</h2>
+<ul>
+<li class="fragment"><a
+href="https://github.com/norm2782/NanoProlog">NanoProlog</a></li>
+<li class="fragment"><a
+href="https://github.com/abailly/hslogic">hslogic</a></li>
+<li class="fragment"><a
+href="https://github.com/andrejbauer/plzoo/tree/master/src/miniprolog">miniprolog</a></li>
+</ul>
+</section></section>
+ </div>
+ </div>
+
+ <script src="https://unpkg.com/reveal.js@^5/dist/reveal.js"></script>
+
+ <!-- reveal.js plugins -->
+ <script src="https://unpkg.com/reveal.js@^5/plugin/notes/notes.js"></script>
+ <script src="https://unpkg.com/reveal.js@^5/plugin/search/search.js"></script>
+ <script src="https://unpkg.com/reveal.js@^5/plugin/zoom/zoom.js"></script>
+
+ <script>
+
+ // Full list of configuration options available at:
+ // https://revealjs.com/config/
+ Reveal.initialize({
+ // Display controls in the bottom right corner
+ controls: true,
+
+ // Help the user learn the controls by providing hints, for example by
+ // bouncing the down arrow when they first encounter a vertical slide
+ controlsTutorial: true,
+
+ // Determines where controls appear, "edges" or "bottom-right"
+ controlsLayout: 'bottom-right',
+
+ // Visibility rule for backwards navigation arrows; "faded", "hidden"
+ // or "visible"
+ controlsBackArrows: 'faded',
+
+ // Display a presentation progress bar
+ progress: true,
+
+ // Display the page number of the current slide
+ slideNumber: false,
+
+ // 'all', 'print', or 'speaker'
+ showSlideNumber: 'all',
+
+ // Add the current slide number to the URL hash so that reloading the
+ // page/copying the URL will return you to the same slide
+ hash: true,
+
+ // Start with 1 for the hash rather than 0
+ hashOneBasedIndex: false,
+
+ // Flags if we should monitor the hash and change slides accordingly
+ respondToHashChanges: true,
+
+ // Push each slide change to the browser history
+ history: false,
+
+ // Enable keyboard shortcuts for navigation
+ keyboard: true,
+
+ // Enable the slide overview mode
+ overview: true,
+
+ // Disables the default reveal.js slide layout (scaling and centering)
+ // so that you can use custom CSS layout
+ disableLayout: false,
+
+ // Vertical centering of slides
+ center: true,
+
+ // Enables touch navigation on devices with touch input
+ touch: true,
+
+ // Loop the presentation
+ loop: false,
+
+ // Change the presentation direction to be RTL
+ rtl: false,
+
+ // see https://revealjs.com/vertical-slides/#navigation-mode
+ navigationMode: 'default',
+
+ // Randomizes the order of slides each time the presentation loads
+ shuffle: false,
+
+ // Turns fragments on and off globally
+ fragments: true,
+
+ // Flags whether to include the current fragment in the URL,
+ // so that reloading brings you to the same fragment position
+ fragmentInURL: true,
+
+ // Flags if the presentation is running in an embedded mode,
+ // i.e. contained within a limited portion of the screen
+ embedded: false,
+
+ // Flags if we should show a help overlay when the questionmark
+ // key is pressed
+ help: true,
+
+ // Flags if it should be possible to pause the presentation (blackout)
+ pause: true,
+
+ // Flags if speaker notes should be visible to all viewers
+ showNotes: false,
+
+ // Global override for autoplaying embedded media (null/true/false)
+ autoPlayMedia: null,
+
+ // Global override for preloading lazy-loaded iframes (null/true/false)
+ preloadIframes: null,
+
+ // Number of milliseconds between automatically proceeding to the
+ // next slide, disabled when set to 0, this value can be overwritten
+ // by using a data-autoslide attribute on your slides
+ autoSlide: 0,
+
+ // Stop auto-sliding after user input
+ autoSlideStoppable: true,
+
+ // Use this method for navigation when auto-sliding
+ autoSlideMethod: null,
+
+ // Specify the average time in seconds that you think you will spend
+ // presenting each slide. This is used to show a pacing timer in the
+ // speaker view
+ defaultTiming: null,
+
+ // Enable slide navigation via mouse wheel
+ mouseWheel: false,
+
+ // The display mode that will be used to show slides
+ display: 'block',
+
+ // Hide cursor if inactive
+ hideInactiveCursor: true,
+
+ // Time before the cursor is hidden (in ms)
+ hideCursorTime: 5000,
+
+ // Opens links in an iframe preview overlay
+ previewLinks: false,
+
+ // Transition style (none/fade/slide/convex/concave/zoom)
+ transition: 'slide',
+
+ // Transition speed (default/fast/slow)
+ transitionSpeed: 'default',
+
+ // Transition style for full page slide backgrounds
+ // (none/fade/slide/convex/concave/zoom)
+ backgroundTransition: 'fade',
+
+ // Number of slides away from the current that are visible
+ viewDistance: 3,
+
+ // Number of slides away from the current that are visible on mobile
+ // devices. It is advisable to set this to a lower number than
+ // viewDistance in order to save resources.
+ mobileViewDistance: 2,
+
+ // reveal.js plugins
+ plugins: [
+ RevealNotes,
+ RevealSearch,
+ RevealZoom
+ ]
+ });
+ </script>
+ </body>
+</html>
diff --git a/prolog/README.md b/prolog/README.md
index d9d6ca0..2501090 100644
--- a/prolog/README.md
+++ b/prolog/README.md
@@ -1,16 +1,142 @@
-# Implementing Prolog
+---
+title: Implementing Prolog
+subtitle: A λ-Nantes Workshop
+author: arnaud@pankzsoft.com - @abailly.bsky.social
+date: 2025-12-10
+---
-## Basics
+# Usage
-* terms:
- * variables start with upper casae: `X`, `Y`...
- * symbols start with lower case: `s`, `z`, `child`, ...
- * symbols have arity 0 or more : `bob`, `child(X, Y)`, `father(bob, Z)`...
-* clauses:
- * _head_: a single term
- * _premises_: a (possibly empty) list of terms
-* a _data set_ is a list of clauses
-* _queries_ are
+![](star-wars.jpg)
+
+## Example
+
+A _program_ about Star Wars characters (including the crappy recent ones)
+
+## Example - Facts
+
+Simple facts asserting the gender of some characters.
+
+```prolog
+female(leia).
+male(vader).
+male(luke).
+male(kylo).
+```
+
+## Example - Facts
+
+More complex facts asserting a `child`hood _relation_ between some characters.
+
+```prolog
+child(luke, vader).
+child(leia, vader).
+child(kylo, leia).
+```
+
+## Example - Rules
+
+_Rules_ (or _Clauses_) allowing to infer some relation from other relations.
+
+```prolog
+son(X,Y) :- male(X), child(X,Y).
+daughter(X,Y) :- female(X), child(X,Y).
+```
+
+## Example - Rules
+
+More complex rules asserting a transitive relation
+
+```prolog
+grandchild(X,Z) :- child(X,Y), child(Y,Z).
+```
+
+## Example - Query
+
+We can _query_ this program, for example asking who is a grandchild of Darth Vader
+
+```prolog
+> ?- grandchild(X, vader).
+success. Type [Enter] to list solutions.
+>
+[X -> kylo]
+```
+
+## Example - Query
+
+A Prolog query can have several answers:
+
+```prolog
+> ?- child(X, vader).
+success. Type [Enter] to list solutions.
+>
+[X -> luke]
+>
+[X -> leia]
+```
+
+## Example - Query
+
+Or no answer:
+
+```prolog
+> ?- grandchild(leia, X).
+failure
+```
+
+# Implementation
+
+## Terms
+
+* variables start with upper casae: `X`, `Y`...
+* symbols start with lower case: `s`, `z`, `child`, ...
+* symbols have 0 or more arguments, e.g an _arity_ : `bob`, `child(X, Y)`, `father(bob, Z)`...
+
+## Clauses
+
+* _head_: a single term
+* _premises_: a (possibly empty) list of terms
+* a _data set_ (or a _program_) is a list of clauses or _facts_
+* a _query_ is a term introduced with `?-`
+
+## Basic algorithm
+
+Given a query and a set of clauses, a Prolog interpreter loop goes like:
+
+1. Push _query_ on its goal stack
+2. Pop up current _goal_ from the stack
+3. Try to match _goal_ with each _clause_:
+ a. _Unify_ goal with the _head_ of _clause_ with _fresh_ variables
+ b. If unification succeeds, push _premises_ of clause onto goals stack
+4. Query succeeds if stack is empty with a successful match
+
+## Unification
+
+Given two terms $t_1$ and $t_2$ with _free variables_ $fv(t_1)$, $fv(t_2)$,
+unification is the process of defining a _substitution_ between variables and _terms_
+
+$$
+\sigma : fv(t_1) \cup fv(t_2) \rightarrow T
+$$
+
+## Unification
+
+* Two variables unify with each other
+* A variable unifies with a term if not already mapped
+* Two relations unify with each other iff
+ * Their symbol is the same
+ * Their arguments unify with each other
+
+## Unification
+
+* $\sigma(X, Y) = \{ X \mapsto Y \}$
+* $\sigma(X, foo) = \{ X \mapsto foo \}$
+* $\sigma(foo, X) = \{ X \mapsto foo \}$
+* $\sigma(foo(bar, Y), foo(X, Z)) = \{ X \mapsto bar, Y \mapsto Z \}$
+
+# Practice
+
+![](workbench.jpg)
## References
diff --git a/prolog/star-wars.jpg b/prolog/star-wars.jpg
new file mode 100644
index 0000000..1b9561f
--- /dev/null
+++ b/prolog/star-wars.jpg
Binary files differ
diff --git a/prolog/workbench.jpg b/prolog/workbench.jpg
new file mode 100644
index 0000000..f81de1a
--- /dev/null
+++ b/prolog/workbench.jpg
Binary files differ