mirror of
https://github.com/NotXia/unibo-ai-notes.git
synced 2025-12-15 19:12:22 +01:00
Add FAIKR2 Prolog basics
This commit is contained in:
@ -0,0 +1,119 @@
|
|||||||
|
<mxfile host="app.diagrams.net" modified="2023-12-04T19:40:43.451Z" agent="Mozilla/5.0 (X11; Linux x86_64; rv:120.0) Gecko/20100101 Firefox/120.0" etag="uMDQyt2wpH4CzOYV8MdK" version="22.1.5" type="device">
|
||||||
|
<diagram name="Pagina-1" id="Kx4IccF5TP9m-yPugrQJ">
|
||||||
|
<mxGraphModel dx="819" dy="414" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
|
||||||
|
<root>
|
||||||
|
<mxCell id="0" />
|
||||||
|
<mxCell id="1" parent="0" />
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-19" value="" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="160" y="390" width="170" height="50" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-25" value="" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="474" y="390" width="210" height="50" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-1" value="<font face="Courier New" style="font-size: 16px;">:- city(X), ~capital(X)<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="269" y="240" width="290" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-2" value="<font face="Courier New" style="font-size: 16px;">:- capital(X), ~capital(X).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="80" y="290" width="330" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-3" value="<font face="Courier New" style="font-size: 16px;">:- region_capital(X), ~capital(X).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="414" y="290" width="330" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-4" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-2" target="nmuJ0MsZKHHojjxWRflp-1">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="390" y="390" as="sourcePoint" />
|
||||||
|
<mxPoint x="440" y="340" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-5" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-3" target="nmuJ0MsZKHHojjxWRflp-1">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="390" y="390" as="sourcePoint" />
|
||||||
|
<mxPoint x="440" y="340" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-7" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-8" target="nmuJ0MsZKHHojjxWRflp-2">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="285" y="360" as="sourcePoint" />
|
||||||
|
<mxPoint x="410" y="360" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-9" value="<font style="font-size: 16px;" face="Courier New">X/rome</font>" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontStyle=1" vertex="1" connectable="0" parent="nmuJ0MsZKHHojjxWRflp-7">
|
||||||
|
<mxGeometry x="-0.0095" y="1" relative="1" as="geometry">
|
||||||
|
<mxPoint x="45" as="offset" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-8" value="<font face="Courier New" style="font-size: 16px;">:- ~capital(rome).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="120" y="340" width="250" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-11" value="<font face="Courier New" style="font-size: 16px;">:- ~capital(bologna).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="454" y="340" width="250" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-13" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-11" target="nmuJ0MsZKHHojjxWRflp-3">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="219" y="360" as="sourcePoint" />
|
||||||
|
<mxPoint x="219" y="330" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-14" value="<font face="Courier New" style="font-size: 16px;">X/bologna</font>" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontSize=16;fontStyle=1" vertex="1" connectable="0" parent="nmuJ0MsZKHHojjxWRflp-13">
|
||||||
|
<mxGeometry x="-0.0095" y="1" relative="1" as="geometry">
|
||||||
|
<mxPoint x="61" y="1" as="offset" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-15" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-16" target="nmuJ0MsZKHHojjxWRflp-8">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="240" y="410" as="sourcePoint" />
|
||||||
|
<mxPoint x="410" y="390" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-16" value="<font face="Courier New" style="font-size: 16px;">:- capital(rome).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="160" y="390" width="170" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-17" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-18" target="nmuJ0MsZKHHojjxWRflp-16">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="245" y="440" as="sourcePoint" />
|
||||||
|
<mxPoint x="340" y="390" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-18" value="success" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="160" y="420" width="170" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-20" value="fail" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="155" y="460" width="180" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-21" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-20" target="nmuJ0MsZKHHojjxWRflp-19">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="280" y="480" as="sourcePoint" />
|
||||||
|
<mxPoint x="330" y="430" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-22" value="<font face="Courier New" style="font-size: 16px;">:- capital(bologna).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="474" y="390" width="210" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-23" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-24" target="nmuJ0MsZKHHojjxWRflp-22">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="579" y="440" as="sourcePoint" />
|
||||||
|
<mxPoint x="674" y="390" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-24" value="success" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="494" y="420" width="170" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-26" value="success" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="489" y="460" width="180" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-27" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-26" target="nmuJ0MsZKHHojjxWRflp-25">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="614" y="480" as="sourcePoint" />
|
||||||
|
<mxPoint x="664" y="430" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-28" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-25" target="nmuJ0MsZKHHojjxWRflp-11">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="219" y="400" as="sourcePoint" />
|
||||||
|
<mxPoint x="219" y="380" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
</root>
|
||||||
|
</mxGraphModel>
|
||||||
|
</diagram>
|
||||||
|
</mxfile>
|
||||||
Binary file not shown.
@ -0,0 +1,48 @@
|
|||||||
|
<mxfile host="app.diagrams.net" modified="2023-12-04T19:49:45.540Z" agent="Mozilla/5.0 (X11; Linux x86_64; rv:120.0) Gecko/20100101 Firefox/120.0" etag="OVwBp_VzQABEGGRmPteH" version="22.1.5" type="device">
|
||||||
|
<diagram name="Pagina-1" id="Kx4IccF5TP9m-yPugrQJ">
|
||||||
|
<mxGraphModel dx="1195" dy="604" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
|
||||||
|
<root>
|
||||||
|
<mxCell id="0" />
|
||||||
|
<mxCell id="1" parent="0" />
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-19" value="" style="rounded=0;whiteSpace=wrap;html=1;fillColor=none;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="329" y="290" width="170" height="70" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-1" value="<font face="Courier New" style="font-size: 16px;">:- ~capital(X), </font><font face="Courier New" style="font-size: 16px;">city(X) </font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="269" y="240" width="290" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-15" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-16" target="nmuJ0MsZKHHojjxWRflp-1">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="240" y="410" as="sourcePoint" />
|
||||||
|
<mxPoint x="245" y="370" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-16" value="<font face="Courier New" style="font-size: 16px;">:- capital(rome).<br style="font-size: 16px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="329" y="290" width="170" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-17" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-18" target="nmuJ0MsZKHHojjxWRflp-16">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="414" y="340" as="sourcePoint" />
|
||||||
|
<mxPoint x="509" y="290" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-31" value="<font style="font-size: 16px;" face="Courier New">X/rome</font>" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontStyle=1" vertex="1" connectable="0" parent="nmuJ0MsZKHHojjxWRflp-17">
|
||||||
|
<mxGeometry x="0.6" y="1" relative="1" as="geometry">
|
||||||
|
<mxPoint x="37" y="12" as="offset" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-18" value="success" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="369.5" y="340" width="89" height="20" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-20" value="fail" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Courier New;fontSize=16;fontStyle=1" vertex="1" parent="1">
|
||||||
|
<mxGeometry x="324" y="380" width="180" height="30" as="geometry" />
|
||||||
|
</mxCell>
|
||||||
|
<mxCell id="nmuJ0MsZKHHojjxWRflp-21" value="" style="endArrow=none;html=1;rounded=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;fontStyle=1" edge="1" parent="1" source="nmuJ0MsZKHHojjxWRflp-20" target="nmuJ0MsZKHHojjxWRflp-19">
|
||||||
|
<mxGeometry width="50" height="50" relative="1" as="geometry">
|
||||||
|
<mxPoint x="449" y="380" as="sourcePoint" />
|
||||||
|
<mxPoint x="499" y="330" as="targetPoint" />
|
||||||
|
</mxGeometry>
|
||||||
|
</mxCell>
|
||||||
|
</root>
|
||||||
|
</mxGraphModel>
|
||||||
|
</diagram>
|
||||||
|
</mxfile>
|
||||||
Binary file not shown.
@ -7,6 +7,7 @@
|
|||||||
|
|
||||||
\makenotesfront
|
\makenotesfront
|
||||||
\input{sections/_logic.tex}
|
\input{sections/_logic.tex}
|
||||||
|
\input{sections/_prolog.tex}
|
||||||
\input{sections/_ontologies.tex}
|
\input{sections/_ontologies.tex}
|
||||||
\input{sections/_descriptive_logic.tex}
|
\input{sections/_descriptive_logic.tex}
|
||||||
\input{sections/_semantic_web.tex}
|
\input{sections/_semantic_web.tex}
|
||||||
|
|||||||
287
src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
Normal file
287
src/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
Normal file
@ -0,0 +1,287 @@
|
|||||||
|
\chapter{Prolog}
|
||||||
|
|
||||||
|
|
||||||
|
It may be useful to first have a look at the "Logic programming" section of
|
||||||
|
\href{https://github.com/NotXia/unibo-ai-notes/tree/pdfs/languages-and-algorithms-for-ai/module2}{\texttt{Languages and Algorithms for AI (module 2)}}.
|
||||||
|
|
||||||
|
|
||||||
|
\section{Syntax}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Term] \marginnote{Term}
|
||||||
|
Following the first-order logic definition, a term can be a:
|
||||||
|
\begin{itemize}
|
||||||
|
\item Constant (\texttt{lowerCase}).
|
||||||
|
\item Variable (\texttt{UpperCase}).
|
||||||
|
\item Function symbol (\texttt{f(t1, \dots, tn)} with \texttt{t1}, \dots, \texttt{tn} terms).
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
\item[Atomic formula] \marginnote{Atomic formula}
|
||||||
|
An atomic formula has form:
|
||||||
|
\[ \texttt{p(t1, \dots, tn)} \]
|
||||||
|
where \texttt{p} is a predicate symbol and \texttt{t1}, \dots, \texttt{tn} are terms.
|
||||||
|
|
||||||
|
Note: there are no syntactic distinctions between constants, functions and predicates.
|
||||||
|
|
||||||
|
\item[Clause] \marginnote{Horn clause}
|
||||||
|
A Prolog program is a set of horn clauses:
|
||||||
|
\begin{descriptionlist}
|
||||||
|
\item[Fact] \texttt{A.}
|
||||||
|
\item[Rule] \texttt{A :- B1, \dots, Bn.} (\texttt{A} is the head and \texttt{B1, \dots, Bn} the body)
|
||||||
|
\item[Goal] \texttt{:- B1, \dots, Bn.}
|
||||||
|
\end{descriptionlist}
|
||||||
|
where:
|
||||||
|
\begin{itemize}
|
||||||
|
\item \texttt{A}, \texttt{B1}, \dots, \texttt{Bn} are atomic formulas.
|
||||||
|
\item \texttt{,} represents the conjunction ($\land$).
|
||||||
|
\item \texttt{:-} represents the logical implication ($\Leftarrow$).
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Quantification] \marginnote{Quantification} \phantom{}
|
||||||
|
\begin{description}
|
||||||
|
\item[Facts]
|
||||||
|
Variables appearing in a fact are quantified universally.
|
||||||
|
\[ \texttt{A(X).} \equiv \forall \texttt{X}: \texttt{A(X)} \]
|
||||||
|
\item[Rules]
|
||||||
|
Variables appearing the the body only are quantified existentially.
|
||||||
|
Variables appearing in both the head and the body are quantified universally.
|
||||||
|
\[ \texttt{A(X) :- B(X, Y).} \equiv \forall \texttt{X}, \exists \texttt{Y} : \texttt{A(X)} \Leftarrow \texttt{B(X, Y)} \]
|
||||||
|
|
||||||
|
\item[Goals]
|
||||||
|
Variables are quantified existentially.
|
||||||
|
\[ \texttt{:- B(Y).} \equiv \exists \texttt{Y} : \texttt{B(Y)} \]
|
||||||
|
\end{description}
|
||||||
|
\end{description}
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
|
||||||
|
\section{Semantics}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Execution of a program]
|
||||||
|
A computation in Prolog attempts to prove the goal.
|
||||||
|
Given a program $P$ and a goal \texttt{:- p(t1, \dots, tn)},
|
||||||
|
the objective is to find a substitution $\sigma$ such that:
|
||||||
|
\[ P \models [\, \texttt{p(t1, \dots, tn)} \,]\sigma \]
|
||||||
|
|
||||||
|
In practice, it uses two stacks:
|
||||||
|
\begin{descriptionlist}
|
||||||
|
\item[Execution stack] Contains the predicates the interpreter is trying to prove.
|
||||||
|
\item[Backtracking stack] Contains the choice points (clauses) the interpreter can try.
|
||||||
|
\end{descriptionlist}
|
||||||
|
|
||||||
|
\item[SLD resolution] \marginnote{SLD}
|
||||||
|
Prolog uses SLD resolution with the following choices:
|
||||||
|
\begin{descriptionlist}
|
||||||
|
\item[Left-most] Always proves the left-most literal first.
|
||||||
|
\item[Depth-first] Applies the predicates following the order of definition.
|
||||||
|
\end{descriptionlist}
|
||||||
|
|
||||||
|
Note that the depth-first approach can be efficiently implemented (tail recursion)
|
||||||
|
but the termination of a Prolog program on a provable goal is not guaranteed as it may loop depending on the ordering of the clauses.
|
||||||
|
|
||||||
|
\item[Disjunction operator]
|
||||||
|
The operator \texttt{;} can be seen as a disjunction and makes the Prolog interpreter
|
||||||
|
explore the remaining SLD tree looking for alternative solutions.
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
\section{Arithmetic operators}
|
||||||
|
\marginnote{Arithmetic operators}
|
||||||
|
|
||||||
|
In Prolog:
|
||||||
|
\begin{itemize}
|
||||||
|
\item Integers and floating points are built-in atoms.
|
||||||
|
\item Math operators are built-in function symbols.
|
||||||
|
\end{itemize}
|
||||||
|
Therefore, mathematical expressions are terms.
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[\texttt{is} predicate]
|
||||||
|
The predicate \texttt{is} is used to evaluate and unify expressions:
|
||||||
|
\[ \texttt{T is Expr} \]
|
||||||
|
where \texttt{T} is a numerical atom or a variable and \texttt{Expr} is an expression without free variables.
|
||||||
|
After evaluation, the result of \texttt{Expr} is unified with \texttt{T}.
|
||||||
|
|
||||||
|
\begin{example} \phantom{}
|
||||||
|
\begin{lstlisting}[language={}]
|
||||||
|
:- X is 2+3.
|
||||||
|
yes X=5
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{example}
|
||||||
|
|
||||||
|
Note: a term representing an expression is evaluated only with the predicate \texttt{is} (otherwise it remains as is).
|
||||||
|
|
||||||
|
\item[Relational operators]
|
||||||
|
Relational operators (\texttt{>}, \texttt{<}, \texttt{>=}, \texttt{=<}, \texttt{==}, \texttt{=/=}) are built-in.
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
\section{Lists}
|
||||||
|
\marginnote{Lists}
|
||||||
|
|
||||||
|
A list is defined recursively as:
|
||||||
|
\begin{descriptionlist}
|
||||||
|
\item[Empty list] \texttt{[]}
|
||||||
|
\item[List constructor] \texttt{.(T, L)} where \texttt{T} is a term and \texttt{L} is a list.
|
||||||
|
\end{descriptionlist}
|
||||||
|
Note that a list always ends with an empty list.
|
||||||
|
|
||||||
|
As the formal definition is impractical, some syntactic sugar has been defined:
|
||||||
|
\begin{descriptionlist}
|
||||||
|
\item[List definition] \texttt{[t1, \dots, tn]} can be used to define a list.
|
||||||
|
\item[Head and tail] \texttt{[H | T]} where \texttt{H} is the head (term) and \texttt{T} the tail (list) can be useful for recursive calls.
|
||||||
|
\end{descriptionlist}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
\section{Cut}
|
||||||
|
\marginnote{Cut}
|
||||||
|
|
||||||
|
The cut operator (\texttt{!}) allows to control the exploration of the SLD tree.
|
||||||
|
|
||||||
|
A cut in a clause:
|
||||||
|
\[ \texttt{p :- q1, \dots, qi, !, qj, \dots, qn.} \]
|
||||||
|
makes the interpreter consider only the first choice points for \texttt{q1, \dots, qi}, dropping all the other possibilities.
|
||||||
|
Therefore, if \texttt{qj, \dots, qn} fails, there won't be backtracking and \texttt{p} fails.
|
||||||
|
|
||||||
|
\begin{example} \phantom{}\\[0.5em]
|
||||||
|
\begin{minipage}{0.5\textwidth}
|
||||||
|
\begin{lstlisting}
|
||||||
|
p(X) :- q(X), r(X).
|
||||||
|
q(1).
|
||||||
|
q(2).
|
||||||
|
r(2).
|
||||||
|
|
||||||
|
:- p(X).
|
||||||
|
yes X=2
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{0.5\textwidth}
|
||||||
|
\begin{lstlisting}
|
||||||
|
p(X) :- q(X), !, r(X).
|
||||||
|
q(1).
|
||||||
|
q(2).
|
||||||
|
r(2).
|
||||||
|
|
||||||
|
:- p(X).
|
||||||
|
no
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
|
||||||
|
In the second case, the cut drops the choice point \texttt{q(2)} and only considers \texttt{q(1)}.
|
||||||
|
\end{example}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Mutual exclusion]
|
||||||
|
A cut can be useful to achieve mutual exclusion.
|
||||||
|
In other words, to represent a conditional branching:
|
||||||
|
\[ \texttt{if a(X) then b else c} \]
|
||||||
|
a cut can be used as follows:
|
||||||
|
\begin{lstlisting}
|
||||||
|
p(X) :- a(X), !, b.
|
||||||
|
p(X) :- c.
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
If \texttt{a(X)} succeeds, other choice points for \texttt{p} will be dropped and only \texttt{b} will be evaluated.
|
||||||
|
If \texttt{a(X)} fails, the second clause will be considered, therefore evaluating \texttt{c}.
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
\section{Negation}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Closed-world assumption] \marginnote{Closed-world assumption}
|
||||||
|
Only what is stated in a program $P$ is true, everything else is false:
|
||||||
|
\[ \texttt{CWA}(P) = P \cup \{ \lnot A \mid A \text{ is a ground atomic formula and } P \cancel{\models} A \} \]
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Non-monotonic inference rule]
|
||||||
|
Adding new axioms to the program may change the set of valid theorems.
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
As first-order logic in undecidable, closed-world assumption cannot be directly applied in practice.
|
||||||
|
|
||||||
|
\item[Negation as failure] \marginnote{Negation as failure}
|
||||||
|
A negated atom $\lnot A$ is considered true iff $A$ fails in finite time:
|
||||||
|
\[ \texttt{NF}(P) = P \cup \{ \lnot A \mid A \in \texttt{FF}(P) \} \]
|
||||||
|
where $\texttt{FF}(P) = \{ B \mid P \cancel{\models} B \text{ in finite time} \}$
|
||||||
|
is the set of atoms for which the proof fails in finite time.
|
||||||
|
Note that not all atoms $B$ such that $P \cancel{\models} B$ are in $\texttt{FF}(P)$.
|
||||||
|
|
||||||
|
\item[SLDNF] \marginnote{SLDNF}
|
||||||
|
SLD resolution with NF to solve negative atoms.
|
||||||
|
|
||||||
|
Given a goal of literals \texttt{:- L$_1$, \dots, L$_m$}, SLDNF does the following:
|
||||||
|
\begin{enumerate}
|
||||||
|
\item Select a positive or ground negative literal \texttt{L$_i$}:
|
||||||
|
\begin{itemize}
|
||||||
|
\item If \texttt{L$_i$} is positive, apply the normal SLD resolution.
|
||||||
|
\item If \texttt{L$_i$} = $\lnot A$, prove that $A$ fails in finite time.
|
||||||
|
If it succeeds, \texttt{L$_i$} fails.
|
||||||
|
\end{itemize}
|
||||||
|
\item Solve the goal \texttt{:- L$_1$, \dots, L$_{i-1}$, L$_{i+1}$, \dots L$_m$}.
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
\begin{theorem}
|
||||||
|
If only positive or ground negative literal are selected during resolution, SLDNF is correct and complete.
|
||||||
|
\end{theorem}
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[Prolog SLDNF]
|
||||||
|
Prolog uses an incorrect implementation of SLDNF where the selection rule always chooses the left-most literal.
|
||||||
|
This potentially causes incorrect deductions.
|
||||||
|
|
||||||
|
\begin{proof}
|
||||||
|
When proving \texttt{:- \char`\\+capital(X).}, the intended meaning is:
|
||||||
|
\[ \exists \texttt{X}: \lnot \texttt{capital(X)} \]
|
||||||
|
|
||||||
|
In SLDNF, to prove \texttt{:- \char`\\+capital(X).}, the algorithm proves \texttt{:- capital(X).}, which results in:
|
||||||
|
\[ \exists \texttt{X}: \texttt{capital(X)} \]
|
||||||
|
and then negates the result, which corresponds to:
|
||||||
|
\[ \lnot (\exists \texttt{X}: \texttt{capital(X)}) \iff \forall \texttt{X}: (\lnot \texttt{capital(X)}) \]
|
||||||
|
|
||||||
|
\end{proof}
|
||||||
|
|
||||||
|
\begin{example}[Correct SLDNF resolution]
|
||||||
|
Given the program:
|
||||||
|
\begin{lstlisting}[language={}, mathescape=true]
|
||||||
|
capital(rome).
|
||||||
|
region_capital(bologna).
|
||||||
|
city(X) :- capital(X).
|
||||||
|
city(X) :- region_capital(X).
|
||||||
|
|
||||||
|
:- city(X), \+capital(X).
|
||||||
|
\end{lstlisting}
|
||||||
|
its resolution succeeds with \texttt{X=bologna} as \texttt{\char`\\+capital(X)} is ground by the unification of \texttt{city(X)}.
|
||||||
|
\begin{center}
|
||||||
|
\includegraphics[width=0.75\textwidth]{img/_sldnf_correct_example.pdf}
|
||||||
|
\end{center}
|
||||||
|
\end{example}
|
||||||
|
|
||||||
|
\begin{example}[Incorrect SLDNF resolution]
|
||||||
|
Given the program: \\
|
||||||
|
\begin{minipage}{0.45\textwidth}
|
||||||
|
\begin{lstlisting}[language={}, mathescape=true]
|
||||||
|
capital(rome).
|
||||||
|
region_capital(bologna).
|
||||||
|
city(X) :- capital(X).
|
||||||
|
city(X) :- region_capital(X).
|
||||||
|
|
||||||
|
:- \+capital(X), city(X).
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{0.5\textwidth}
|
||||||
|
\includegraphics[width=0.7\linewidth]{img/_sldnf_incorrect_example.pdf}
|
||||||
|
\end{minipage}
|
||||||
|
|
||||||
|
its resolution fails as \texttt{\char`\\+capital(X)} is a free variable and
|
||||||
|
the proof of \texttt{capital(X)} is ground with \texttt{X=rome} and succeeds, therefore failing \texttt{\char`\\+capital(X)}.
|
||||||
|
Note that \texttt{bologna} is not tried as it does not appear in the axioms of \texttt{capital}.
|
||||||
|
\end{example}
|
||||||
|
\end{description}
|
||||||
|
\end{description}
|
||||||
Reference in New Issue
Block a user