mirror of
https://github.com/NotXia/unibo-ai-notes.git
synced 2025-12-16 19:32:21 +01:00
Moved FAIKR2 in year1
This commit is contained in:
1
src/year1/fundamentals-of-ai-and-kr/module2/ainotes.cls
Symbolic link
1
src/year1/fundamentals-of-ai-and-kr/module2/ainotes.cls
Symbolic link
@ -0,0 +1 @@
|
||||
../../../ainotes.cls
|
||||
21
src/year1/fundamentals-of-ai-and-kr/module2/faikr2.tex
Normal file
21
src/year1/fundamentals-of-ai-and-kr/module2/faikr2.tex
Normal file
@ -0,0 +1,21 @@
|
||||
\documentclass[11pt]{ainotes}
|
||||
|
||||
\title{Fundamentals of Artificial Intelligence and Knowledge Representation\\(Module 2)}
|
||||
\date{2023 -- 2024}
|
||||
\def\lastupdate{{PLACEHOLDER-LAST-UPDATE}}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\makenotesfront
|
||||
\input{sections/_logic.tex}
|
||||
\input{sections/_prolog.tex}
|
||||
\input{sections/_ontologies.tex}
|
||||
\input{sections/_descriptive_logic.tex}
|
||||
\input{sections/_semantic_web.tex}
|
||||
\input{sections/_time_reasoning.tex}
|
||||
\input{sections/_probabilistic_reasoning.tex}
|
||||
\input{sections/_forward_reasoning.tex}
|
||||
\input{sections/_business_process.tex}
|
||||
\eoc
|
||||
|
||||
\end{document}
|
||||
@ -0,0 +1,34 @@
|
||||
<mxfile host="app.diagrams.net" modified="2023-12-08T19:47:25.292Z" agent="Mozilla/5.0 (X11; Linux x86_64; rv:120.0) Gecko/20100101 Firefox/120.0" etag="OSZXvqEczNiZXNqwfc7z" version="22.1.7" type="device">
|
||||
<diagram name="Pagina-1" id="ed2_-DnoGlUrIFm0Tw4G">
|
||||
<mxGraphModel dx="989" dy="500" 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="ZAoLLnpvm8W4UGgeYZgy-1" value="<div style="font-size: 16px;"><font style="font-size: 16px;">sneezing(bob) :- flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">sneezing(bob) :- hay_fever(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">hay_fever(bob).<br style="font-size: 16px;"></font></div><div style="font-size: 16px;"><font style="font-size: 16px;"><br style="font-size: 16px;"></font></div>" style="rounded=0;whiteSpace=wrap;html=1;align=left;verticalAlign=top;fontFamily=Courier New;fontSize=16;fontStyle=1" parent="1" vertex="1">
|
||||
<mxGeometry x="80" y="250" width="320" height="90" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-2" value="<div style="font-size: 16px;"><font style="font-size: 16px;">null :- flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">sneezing(bob) :- hay_fever(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">hay_fever(bob).<br style="font-size: 16px;"></font></div><div style="font-size: 16px;"><font style="font-size: 16px;"><br style="font-size: 16px;"></font></div>" style="rounded=0;whiteSpace=wrap;html=1;align=left;verticalAlign=top;fontFamily=Courier New;fontSize=16;fontStyle=1" parent="1" vertex="1">
|
||||
<mxGeometry x="420" y="250" width="320" height="90" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-3" value="<font style="font-size: 20px;">P</font><font style="font-size: 20px;">(w<sub style="font-size: 20px;">1</sub>) = 0.7 · 0.8<br style="font-size: 20px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Times New Roman;fontSize=20;" parent="1" vertex="1">
|
||||
<mxGeometry x="80" y="220" width="320" height="30" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-4" value="<font style="font-size: 20px;">P</font><font style="font-size: 20px;">(w<sub style="font-size: 20px;">2</sub>) = 0.3 · 0.8<br style="font-size: 20px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Times New Roman;fontSize=20;" parent="1" vertex="1">
|
||||
<mxGeometry x="420" y="220" width="320" height="30" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-5" value="<div style="font-size: 16px;"><font style="font-size: 16px;">sneezing(bob) :- flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">null :- hay_fever(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">hay_fever(bob).<br style="font-size: 16px;"></font></div><div style="font-size: 16px;"><font style="font-size: 16px;"><br style="font-size: 16px;"></font></div>" style="rounded=0;whiteSpace=wrap;html=1;align=left;verticalAlign=top;fontFamily=Courier New;fontSize=16;fontStyle=1" parent="1" vertex="1">
|
||||
<mxGeometry x="80" y="390" width="320" height="90" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-6" value="<div style="font-size: 16px;"><font style="font-size: 16px;">null :- flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">null :- hay_fever(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">flu(bob).</font></div><div style="font-size: 16px;"><font style="font-size: 16px;">hay_fever(bob).<br style="font-size: 16px;"></font></div><div style="font-size: 16px;"><font style="font-size: 16px;"><br style="font-size: 16px;"></font></div>" style="rounded=0;whiteSpace=wrap;html=1;align=left;verticalAlign=top;fontFamily=Courier New;fontSize=16;fontStyle=1" parent="1" vertex="1">
|
||||
<mxGeometry x="420" y="390" width="320" height="90" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-7" value="<font style="font-size: 20px;">P</font><font style="font-size: 20px;">(w<sub style="font-size: 20px;">3</sub>) = 0.7 · 0.2<br style="font-size: 20px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Times New Roman;fontSize=20;" parent="1" vertex="1">
|
||||
<mxGeometry x="80" y="360" width="320" height="30" as="geometry" />
|
||||
</mxCell>
|
||||
<mxCell id="ZAoLLnpvm8W4UGgeYZgy-8" value="<font style="font-size: 20px;">P</font><font style="font-size: 20px;">(w<sub style="font-size: 20px;">4</sub>) = 0.3 · 0.2<br style="font-size: 20px;"></font>" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Times New Roman;fontSize=20;" parent="1" vertex="1">
|
||||
<mxGeometry x="420" y="360" width="320" height="30" as="geometry" />
|
||||
</mxCell>
|
||||
</root>
|
||||
</mxGraphModel>
|
||||
</diagram>
|
||||
</mxfile>
|
||||
Binary file not shown.
@ -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.
Binary file not shown.
|
After Width: | Height: | Size: 84 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 31 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 37 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 16 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 19 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 18 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 12 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 47 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 20 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 20 KiB |
BIN
src/year1/fundamentals-of-ai-and-kr/module2/img/bpmn_data.png
Normal file
BIN
src/year1/fundamentals-of-ai-and-kr/module2/img/bpmn_data.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 388 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 215 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 14 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 16 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 13 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 13 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 18 KiB |
BIN
src/year1/fundamentals-of-ai-and-kr/module2/img/flower_petri.png
Normal file
BIN
src/year1/fundamentals-of-ai-and-kr/module2/img/flower_petri.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 38 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 180 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 85 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 54 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 75 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 79 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 266 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 57 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 2.8 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 3.7 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 140 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 2.7 KiB |
@ -0,0 +1,652 @@
|
||||
\chapter{Business process management}
|
||||
|
||||
\begin{description}
|
||||
\item[Information system] \marginnote{Information system}
|
||||
Contains static (raw) data partially describing the flow of a business.
|
||||
|
||||
\item[Business process management] \marginnote{Business process management}
|
||||
Methods to design, manage and analyze business processes by mining data contained in information systems.
|
||||
|
||||
Business processes help in making decisions and automation.
|
||||
|
||||
\item[Business process lifecycle] \phantom{}
|
||||
\begin{description}
|
||||
\item[Design and analysis]
|
||||
Definition of models and schemas.
|
||||
\item[Configuration]
|
||||
Execution of the business process.
|
||||
\item[Enactment]
|
||||
Collect and analyze logs to make predictions.
|
||||
\item[Evaluation]
|
||||
Assess the quality of the process.
|
||||
\end{description}
|
||||
|
||||
\item[Business process types] \phantom{}
|
||||
\begin{description}
|
||||
\item[Organizational vs operational] \phantom{}
|
||||
\begin{description}
|
||||
\item[Organizational]
|
||||
Process described with its inputs, outputs, expected outcomes and dependencies.
|
||||
\item[Operational]
|
||||
Process described disregarding its implementation.
|
||||
\end{description}
|
||||
|
||||
\item[Intra-organization vs inter-organization] \phantom{}
|
||||
\begin{description}
|
||||
\item[Intra-organization]
|
||||
Only activities executed within the business boundaries.
|
||||
\item[Inter-organization]
|
||||
Part of the activities are executed outside the business and the process does not have control of them.
|
||||
\end{description}
|
||||
|
||||
\item[Execution properties] \phantom{}
|
||||
\begin{description}
|
||||
\item[Degree of automation]
|
||||
\item[Degree of repetition]
|
||||
\item[Degree of structuring]
|
||||
\end{description}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Business process modeling}
|
||||
|
||||
\begin{description}
|
||||
\item[Activity instance] \marginnote{Activity instance}
|
||||
Represents the actual work done during the execution of a business process.
|
||||
|
||||
An activity instance can be described as a sequence of temporally ordered events.
|
||||
Formally, an activity instance $i$ is defined as:
|
||||
\[ i = (E_i, <_i) \]
|
||||
where $E_i \subseteq \{ i_i, e_i, b_i, t_i \}$ is an event with:
|
||||
\begin{itemize}
|
||||
\item $i_i$ for initialization;
|
||||
\item $e_i$ for enabling;
|
||||
\item $b_i$ for beginning;
|
||||
\item $t_i$ for terminating.
|
||||
\end{itemize}
|
||||
$<_i$ is a relation order such that $<_i \subseteq \{ (i_i, e_i), (e_i, b_i), (b_i, t_i) \}$.
|
||||
|
||||
\item[Activity model] \marginnote{Activity model}
|
||||
Describes a set of similar activity instances.
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Control flow modeling}
|
||||
|
||||
\begin{description}
|
||||
\item[Process modeling types] \phantom{}
|
||||
\begin{description}
|
||||
\item[Procedural vs declarative] \phantom{}
|
||||
\begin{description}
|
||||
\item[Procedural] \marginnote{Procedural modeling}
|
||||
Based on a strict ordering of the steps.
|
||||
Uses conditional choices, loops, parallel execution, events.
|
||||
|
||||
Subject to the spaghetti-like process problem.
|
||||
|
||||
\item[Declarative] \marginnote{Declarative modeling}
|
||||
Based on the properties that should hold during execution.
|
||||
Uses concepts such as executions, expected executions, prohibited executions.
|
||||
\end{description}
|
||||
|
||||
\item[Closed vs open] \phantom{}
|
||||
\begin{description}
|
||||
\item[Closed] \marginnote{Closed modeling}
|
||||
The execution of non-modelled activities is prohibited.
|
||||
|
||||
\item[Open] \marginnote{Open modeling}
|
||||
Constraints to allow non-modelled activities.
|
||||
\end{description}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
The most common combination of approaches are:
|
||||
\begin{descriptionlist}
|
||||
\item[Closed procedural process modeling]
|
||||
\item[Open declarative process modeling]
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
|
||||
\section{Closed procedural process modeling}
|
||||
|
||||
\begin{description}
|
||||
\item[Process model]
|
||||
Set of process instances with a similar structure described as a graph.
|
||||
|
||||
\begin{description}
|
||||
\item[Edges] Directed arcs to describe temporal orderings.
|
||||
|
||||
\item[Nodes] Nodes can be:
|
||||
\begin{description}
|
||||
\item[Activity models] \marginnote{Activity}
|
||||
Unit of work.
|
||||
\item[Event models] \marginnote{Event}
|
||||
Capture the events that involve activities.
|
||||
\item[Gateway models] \marginnote{Gateway}
|
||||
Control flow constructs.
|
||||
Basic patterns are: \texttt{sequence}, \texttt{and split}, \texttt{and join}, \texttt{exclusive or split}, \texttt{exclusive or join}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
\begin{example}
|
||||
Activity $A$ is executed before activity $B$ (\texttt{sequence} arc).
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/bp_control_flow_sequence.png}
|
||||
\end{center}
|
||||
\end{example}
|
||||
|
||||
\begin{example}
|
||||
Loop with \texttt{exclusive or splits}.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.5\textwidth]{img/bp_control_flow_loop.png}
|
||||
\end{center}
|
||||
\end{example}
|
||||
|
||||
\begin{example} \phantom{}\\
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
The \texttt{and split} allows to run $B$ and $C$ in parallel.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6\linewidth]{img/bp_control_flow_parallel_split.png}
|
||||
\end{center}
|
||||
\end{minipage}
|
||||
\hspace{0.02\textwidth}
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
The \texttt{and join} allows to wait for both $B$ and $C$ to finish.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6\linewidth]{img/bp_control_flow_parallel_join.png}
|
||||
\end{center}
|
||||
\end{minipage}
|
||||
\end{example}
|
||||
|
||||
\begin{example} \phantom{}\\
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
The \texttt{xor split} allows to run only one activity between $B$ and $C$.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6\linewidth]{img/bp_control_flow_xor_split.png}
|
||||
\end{center}
|
||||
\end{minipage}
|
||||
\hspace{0.02\textwidth}
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
The \texttt{xor join} allows to wait for one activity between $B$ and $C$ to finish.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6\linewidth]{img/bp_control_flow_xor_join.png}
|
||||
\end{center}
|
||||
\end{minipage}
|
||||
\end{example}
|
||||
|
||||
\begin{example}
|
||||
The \texttt{or split} allows to run at least one activity between $B$ and $C$.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.3\textwidth]{img/bp_control_flow_or_split.png}
|
||||
\end{center}
|
||||
\end{example}
|
||||
|
||||
\begin{example}
|
||||
The \texttt{N-out-of-M join} allows to wait until $N$ activities have finished.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.3\textwidth]{img/bp_control_flow_n_out_of_m_join.png}
|
||||
\end{center}
|
||||
\end{example}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\subsection{Petri nets}
|
||||
|
||||
\begin{description}
|
||||
\item[Places] \marginnote{Places}
|
||||
Represent the points of execution of a process.
|
||||
Drawn as empty circles.
|
||||
|
||||
\item[Tokens] \marginnote{Tokens}
|
||||
A token can reside in a place.
|
||||
It marks the current state of the process.
|
||||
Drawn as a small black circle.
|
||||
|
||||
\item[Transitions] \marginnote{Transitions}
|
||||
Have input and output places.
|
||||
Drawn as rectangles.
|
||||
|
||||
\begin{description}
|
||||
\item[Token play]
|
||||
A transition is enabled when all its input places have a token and all its output places have not.
|
||||
An enabled transition can be fired: tokens are removed from the inputs and moved to the outputs.
|
||||
\end{description}
|
||||
|
||||
\item[Connections] \marginnote{Connections}
|
||||
Arcs to connect places and transitions.
|
||||
\end{description}
|
||||
|
||||
\begin{example} \phantom{}
|
||||
\begin{center}
|
||||
\includegraphics[width=0.65\textwidth]{img/petri_net_example1.png}
|
||||
\end{center}
|
||||
Transition $t_2$ is a split. $t_5$ is a join.
|
||||
\end{example}
|
||||
|
||||
\begin{table}[H]
|
||||
\centering
|
||||
\begin{tabular}{c|c}
|
||||
\textbf{Petri nets} & \textbf{Business process modeling} \\
|
||||
\hline
|
||||
Petri net & Process model \\
|
||||
Transitions & Activity models \\
|
||||
Tokens & Instances \\
|
||||
Transition firing & Activity execution \\
|
||||
\end{tabular}
|
||||
\caption{Petri nets and business process modeling concepts equivalence}
|
||||
\end{table}
|
||||
|
||||
|
||||
\subsection{Workflow nets}
|
||||
Restriction of Petri nets.
|
||||
|
||||
\begin{description}
|
||||
\item[Transitions syntactic sugar] \marginnote{Transitions} \phantom{}
|
||||
\begin{center}
|
||||
\includegraphics[width=0.5\textwidth]{img/workflow_nets_transitions.png}
|
||||
\end{center}
|
||||
|
||||
\item[Triggers] \marginnote{Triggers}
|
||||
Can be attached to transitions.
|
||||
\begin{description}
|
||||
\item[Automatic trigger] Activity started automatically (standard behavior).
|
||||
|
||||
\item[User trigger] Activity started on user input.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6cm]{img/workflow_nets_user_trigger.png}
|
||||
\end{center}
|
||||
|
||||
\item[External trigger] Activity started on external events.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6cm]{img/workflow_nets_external_trigger.png}
|
||||
\end{center}
|
||||
|
||||
\item[Time trigger] Activity started at a certain time.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6cm]{img/workflow_nets_time_trigger.png}
|
||||
\end{center}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
\begin{example}[Workflow nets with explicit and implicit \texttt{exclusive or split}]
|
||||
\begin{center}
|
||||
\includegraphics[width=0.6\textwidth]{img/workflow_nets_example1.png}
|
||||
\end{center}
|
||||
\end{example}
|
||||
|
||||
|
||||
|
||||
\subsection{Business process model and notation (BPMN)}
|
||||
De-facto standard for business process representation.
|
||||
|
||||
\begin{description}
|
||||
\item[Basic elements] \phantom{}
|
||||
\begin{description}
|
||||
\item[Activity] \marginnote{Activity}
|
||||
Drawn as rectangles with optional decorations (e.g. a decorator to represent a task under human responsibility).
|
||||
|
||||
\item[Event] \marginnote{Event}
|
||||
Drawn as circles.
|
||||
|
||||
\begin{description}
|
||||
\item[Start event]
|
||||
Indicates where and how (triggers) a process starts.
|
||||
Drawn as a thin-bordered circle.
|
||||
|
||||
\item[Intermediate event]
|
||||
Event occurring after the start of a process but before its end.
|
||||
|
||||
\item[End event]
|
||||
Indicates the end of a process and optionally provides its result.
|
||||
Drawn as a thick-bordered circle.
|
||||
\end{description}
|
||||
|
||||
\item[Flow] \marginnote{Flow}
|
||||
Drawn as arrows.
|
||||
|
||||
\begin{description}
|
||||
\item[Sequence flow]
|
||||
Flow of processes (orchestration).
|
||||
|
||||
\item[Message flow]
|
||||
Communication between processes and external entities.
|
||||
\end{description}
|
||||
|
||||
\item[Gateway] \marginnote{Gateway}
|
||||
Parallel, split and join. Drawn as rhombus.
|
||||
\end{description}
|
||||
|
||||
\item[Pool] \marginnote{Pool}
|
||||
Represent an independent participant with its own business process specification.
|
||||
|
||||
\item[Lanes] \marginnote{Lanes}
|
||||
Resource classes within a pool.
|
||||
|
||||
\item[Data] \marginnote{Data} \phantom{}
|
||||
\begin{description}
|
||||
\item[Data object] Local variable representing a temporary unit of information.
|
||||
\item[Data object reference] Reference to a data object.
|
||||
\item[Data object collection] Collection of data objects.
|
||||
\item[Data store] Persistent unit of information accessed by the process and external entities.
|
||||
\end{description}
|
||||
\begin{figure}[H]
|
||||
\centering
|
||||
\includegraphics[width=0.4\textwidth]{img/bpmn_data.png}
|
||||
\caption{Data symbols}
|
||||
\end{figure}
|
||||
|
||||
\item[Reaction to events] \marginnote{Reactions} \phantom{}
|
||||
\begin{description}
|
||||
\item[Throw] Signals that something happened.
|
||||
\item[Catch] Responds to a signal.
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
\begin{figure}[H]
|
||||
\centering
|
||||
\includegraphics[width=0.6\textwidth]{img/bpmn_example1.png}
|
||||
\caption{Example of BPMN}
|
||||
\end{figure}
|
||||
|
||||
|
||||
|
||||
\section{Open declarative process modeling}
|
||||
|
||||
Define formal properties for process models (i.e. more formal than procedural methods).
|
||||
Properties defined in term of the evolution of the process (similar to the evolution of the world in modal logics)
|
||||
|
||||
|
||||
\subsection{Linear-time temporal logic in BPM}
|
||||
Based on the notion of world. Advancements in the process result in new worlds.
|
||||
|
||||
\begin{description}
|
||||
\item[LTL model] \marginnote{LTL model}
|
||||
An LTL model is a set of events that happened in the execution of an instance of a process.
|
||||
|
||||
\item[LTL execution trace] \marginnote{LTL execution trace}
|
||||
An LTL execution trace is an LTL model based on the set of natural numbers.
|
||||
It represents the evolution of the world.
|
||||
|
||||
\item[Syntax and semantics] Follows from the syntax and semantics of linear-time temporal logic.
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{DECLARE}
|
||||
|
||||
Based on constraints that must hold in every possible execution of the system.
|
||||
|
||||
\begin{description}
|
||||
\item[Atomic activity] \marginnote{Atomic activity}
|
||||
Drawn as boxes.
|
||||
|
||||
\item[Unary constraints] \marginnote{Unary constraints}
|
||||
Defined on atomic activities.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/declare_unary_constraint.png}
|
||||
\end{center}
|
||||
|
||||
\item[Binary constraints] \marginnote{Binary constraints}
|
||||
Connects two activities.
|
||||
|
||||
A solid circle indicates when the constraint is enforced.
|
||||
A directed arrow indicates time ordering.
|
||||
|
||||
\begin{description}
|
||||
\item[Response]
|
||||
An execution of $A$ should be eventually followed by an execution of $B$.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.2\textwidth]{img/declare_response.png}
|
||||
\end{center}
|
||||
|
||||
\item[Chained response]
|
||||
An execution of $A$ should be immediately followed by an execution of $B$.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.2\textwidth]{img/declare_chained_response.png}
|
||||
\end{center}
|
||||
|
||||
\item[Negated response]
|
||||
After the execution of $A$, $B$ cannot be executed anymore.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.2\textwidth]{img/declare_negated_response.png}
|
||||
\end{center}
|
||||
|
||||
\item[Precedence]
|
||||
An execution of $B$ should have been preceded by an execution of $A$.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.2\textwidth]{img/declare_precedence.png}
|
||||
\end{center}
|
||||
\end{description}
|
||||
|
||||
\item[Semantics]
|
||||
The semantics of the constraints can be defined using LTL.
|
||||
|
||||
\item[Verifiable properties] \phantom{}
|
||||
\begin{description}
|
||||
\item[Enactment] \marginnote{Enactment}
|
||||
Determine the next possible activities.
|
||||
\item[Conformance] \marginnote{Conformance}
|
||||
Check if an instance of a process respects the constraints.
|
||||
\item[Interoperability] \marginnote{Interoperability}
|
||||
Determine if two DECLARE systems can be merged.
|
||||
\end{description}
|
||||
|
||||
\item[Limits] \phantom{}
|
||||
\begin{itemize}
|
||||
\item DECLARE cannot represent quantitative temporal constraints.
|
||||
\item Compared to closed procedural methods, it is more difficult to learn models.
|
||||
\end{itemize}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Business process mining}
|
||||
|
||||
\begin{description}
|
||||
\item[Event log] \marginnote{Event log}
|
||||
Sequence of events.
|
||||
Each event (trace) is a sequence of activities.
|
||||
|
||||
\begin{example}
|
||||
$L = \{ \langle \texttt{abcd} \rangle, \langle \texttt{abcd} \rangle, \langle \texttt{acbd} \rangle \}$
|
||||
\end{example}
|
||||
|
||||
\item[Business process mining] \marginnote{Business process mining}
|
||||
Extract knowledge from event logs to improve a process.
|
||||
|
||||
Possible applications are:
|
||||
\begin{itemize}
|
||||
\item Automated process discovery.
|
||||
\item Conformance checking.
|
||||
\item Organizational mining.
|
||||
\item Simulations.
|
||||
\item Process extension.
|
||||
\item Predictions.
|
||||
\end{itemize}
|
||||
|
||||
\item[Process mining types] \phantom{}
|
||||
\begin{description}
|
||||
\item[Discovery] \marginnote{Discovery}
|
||||
Takes as input an event log and outputs a model.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/process_mining_discovery.png}
|
||||
\end{center}
|
||||
|
||||
\item[Conformance checking] \marginnote{Conformance checking}
|
||||
Takes as input an event log and a model and outputs if the log is conformant to the model.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/process_mining_conformance.png}
|
||||
\end{center}
|
||||
|
||||
\item[Enhancement] \marginnote{Enhancement}
|
||||
Takes as input an event log and a model and outputs a new model.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/process_mining_enhancement.png}
|
||||
\end{center}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Process discovery}
|
||||
|
||||
\begin{description}
|
||||
\item[Process discovery] \marginnote{Process discovery}
|
||||
Learn a process model representative of the input event log.
|
||||
|
||||
More formally, a process discovery algorithm is a function that maps an event log into a business process modeling language.
|
||||
In our case, we map logs into Petri nets (preferably workflow nets).
|
||||
|
||||
\begin{remark}
|
||||
Process discovery is a unary classification problem.
|
||||
We are interested in learning a model fitted on the entire event log.
|
||||
\end{remark}
|
||||
|
||||
\item[$\alpha$-algorithm] \marginnote{$\alpha$-algorithm}
|
||||
$\alpha$-algorithm fixes the following interesting relations:
|
||||
\begin{descriptionlist}
|
||||
\item[$>_L$)] $a >_L b$ iff there exists a trace in the event log where $a$ precedes $b$.
|
||||
\item[$\rightarrow_L$)] $a \rightarrow_L b$ iff $a >_L b$ and $b \cancel{>}_L\, a$.
|
||||
\item[$\#_L$)] $a \# b$ iff $a \cancel{>}_L\, b$ and $b \cancel{>}_L\, a$.
|
||||
\item[$\Vert_L$)] $a \Vert_L b$ iff $a >_L b$ and $b >_L a$.
|
||||
\end{descriptionlist}
|
||||
|
||||
$\alpha$-algorithm works as follows:
|
||||
\begin{enumerate}
|
||||
\item Look for the relations in the event log.
|
||||
\item Focus on the most interesting relations and identify the biggest set of involved activities.
|
||||
\item Remove redundancies.
|
||||
\item Represent them as a Petri net.
|
||||
\end{enumerate}
|
||||
|
||||
\begin{example}
|
||||
Given the event log $L = \{ \langle \texttt{abcd} \rangle, \langle \texttt{abcd} \rangle,
|
||||
\langle \texttt{abcd} \rangle, \langle \texttt{acbd} \rangle, \langle \texttt{acbd} \rangle, \langle \texttt{aed} \rangle \}$,
|
||||
we want to apply the $\alpha$-algorithm:
|
||||
\begin{enumerate}
|
||||
\item We determine the relations:
|
||||
\[
|
||||
\begin{split}
|
||||
>_{L_1} &= \{ (\texttt{a}, \texttt{b}), (\texttt{a}, \texttt{c}), (\texttt{a}, \texttt{e}), (\texttt{b}, \texttt{c}),
|
||||
(\texttt{c}, \texttt{b}), (\texttt{b}, \texttt{d}), (\texttt{c}, \texttt{d}), (\texttt{e}, \texttt{d}) \} \\
|
||||
\rightarrow_{L_1} &= \{ (\texttt{a}, \texttt{b}), (\texttt{a}, \texttt{c}), (\texttt{a}, \texttt{e}),
|
||||
(\texttt{b}, \texttt{d}), (\texttt{c}, \texttt{d}), (\texttt{e}, \texttt{d}) \} \\
|
||||
\#_{L_1} &= \{ (\texttt{a}, \texttt{a}), (\texttt{a}, \texttt{d}), (\texttt{b}, \texttt{b}), (\texttt{b}, \texttt{e}), (\texttt{c}, \texttt{c}),
|
||||
(\texttt{c}, \texttt{e}), (\texttt{d}, \texttt{a}), (\texttt{d}, \texttt{d}), (\texttt{e}, \texttt{b}), (\texttt{e}, \texttt{c}), (\texttt{e}, \texttt{e}) \} \\
|
||||
\Vert_{L_1} &= \{ (\texttt{b}, \texttt{c}), (\texttt{c}, \texttt{b}) \}
|
||||
\end{split}
|
||||
\]
|
||||
And construct the footprint matrix:
|
||||
\begin{center}
|
||||
\begin{tabular}{c | c c c c c}
|
||||
& \texttt{a} & \texttt{b} & \texttt{c} & \texttt{d} & \texttt{e} \\
|
||||
\hline
|
||||
\texttt{a} & $\#_{L_1}$ & $\rightarrow_{L_1}$ & $\rightarrow_{L_1}$ & $\#_{L_1}$ & $\rightarrow_{L_1}$ \\
|
||||
\texttt{b} & $\leftarrow_{L_1}$ & $\#_{L_1}$ & $\Vert_{L_1}$ & $\rightarrow_{L_1}$ & $\#_{L_1}$ \\
|
||||
\texttt{c} & $\leftarrow_{L_1}$ & $\Vert_{L_1}$ & $\#_{L_1}$ & $\rightarrow_{L_1}$ & $\#_{L_1}$ \\
|
||||
\texttt{d} & $\#_{L_1}$ & $\leftarrow_{L_1}$ & $\leftarrow_{L_1}$ & $\#_{L_1}$ & $\leftarrow_{L_1}$ \\
|
||||
\texttt{e} & $\leftarrow_{L_1}$ & $\#_{L_1}$ & $\#_{L_1}$ & $\rightarrow_{L_1}$ & $\#_{L_1}$ \\
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
\item We determine the interesting relations as the pair of sets $(P, Q)$ of activities such that:
|
||||
\[ \forall p \in P, q \in Q: (p \rightarrow q) \land (p \# p) \land (q \# q) \]
|
||||
|
||||
This can be algorithmically done by building a footprint table whose rows and columns allow to obtain all the combinations of the activities.
|
||||
Therefore, the set of interesting relations is:
|
||||
\[
|
||||
\begin{split}
|
||||
X_{L_1} = \{
|
||||
(\{\texttt{a}\}, \{\texttt{b}\}), (\{\texttt{a}\}, \{\texttt{c}\}), (\{\texttt{a}\}, \{\texttt{e}\}),
|
||||
(\{\texttt{a}\}, \{\texttt{b}, \texttt{e}\}), (\{\texttt{a}\}, \{\texttt{c}, \texttt{e}\}), \\
|
||||
(\{\texttt{b}\}, \{\texttt{d}\}), (\{\texttt{c}\}, \{\texttt{d}\}), (\{\texttt{e}\}, \{\texttt{d}\}),
|
||||
(\{\texttt{b}, \texttt{e}\}, \{\texttt{d}\}), (\{\texttt{c}, \texttt{e}\}, \{\texttt{d}\})
|
||||
\}
|
||||
\end{split}
|
||||
\]
|
||||
|
||||
\item Then, we remove the redundancies in the set of interesting relations $X_{L_1}$:
|
||||
\[ Y_{L_1} = \{ (\{\texttt{a}\}, \{\texttt{b}, \texttt{e}\}), (\{\texttt{a}\}, \{\texttt{c}, \texttt{e}\}),
|
||||
(\{\texttt{b}, \texttt{e}\}, \{\texttt{d}\}), (\{\texttt{c}, \texttt{e}\}, \{\texttt{d}\}) \} \]
|
||||
It can be seen that all the relations in $X_{L_1}$ can be derived from $Y_{L_1} \subset X_{L_1}$.
|
||||
|
||||
\item With the reduced set of interesting relations, we can build the Petri net.
|
||||
\begin{center}
|
||||
\includegraphics[width=0.5\textwidth]{img/alpha_algorithm_example.png}
|
||||
\end{center}
|
||||
\end{enumerate}
|
||||
\end{example}
|
||||
|
||||
$\alpha$-algorithm has the following limitations:
|
||||
\begin{itemize}
|
||||
\item It can learn unnecessarily complex networks.
|
||||
\item It cannot learn loops.
|
||||
\item The frequency of the traces is not taken into account.
|
||||
\end{itemize}
|
||||
|
||||
|
||||
\item[Model evaluation]
|
||||
Different models can capture the same process described in a log.
|
||||
This allows for models that are capable of capturing all the possible traces of a log but
|
||||
are unable to provide any insight (e.g. flower Petri net).
|
||||
|
||||
\begin{figure}[H]
|
||||
\centering
|
||||
\includegraphics[width=0.4\textwidth]{img/flower_petri.png}
|
||||
\caption{Example of flower Petri net}
|
||||
\end{figure}
|
||||
|
||||
General judging criteria for a model are:
|
||||
\begin{descriptionlist}
|
||||
\item[Fitness] \marginnote{Fitness}
|
||||
How well the model fits the majority of the traces.
|
||||
\item[Simplicity] \marginnote{Simplicity}
|
||||
Based on the structure of the model.
|
||||
\item[Precision] \marginnote{Precision}
|
||||
How the model is able to capture rare cases.
|
||||
\item[Generalization] \marginnote{Generalization}
|
||||
How the model generalizes on the training traces.
|
||||
\end{descriptionlist}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\subsection{Conformance checking}
|
||||
|
||||
\begin{description}
|
||||
\item[Descriptive model discrepancies] \marginnote{Descriptive model}
|
||||
The model needs to be improved.
|
||||
|
||||
\item[Prescriptive model discrepancies] \marginnote{Prescriptive model}
|
||||
The traces need to be checked as the model cannot be changed (e.g. model of the law).
|
||||
The deviation of a trace can be desired or undesired.
|
||||
\end{description}
|
||||
|
||||
\begin{remark}
|
||||
A trace can be seen as a sequence of symbols. It is possible to syntactically check them using a regular expression.
|
||||
\end{remark}
|
||||
|
||||
\begin{description}
|
||||
\item[Token replay] \marginnote{Token replay}
|
||||
Given a trace and a Petri net, the trace is replayed on the model by moving tokens around.
|
||||
The trace is conform if the end event can be reached, otherwise, it is not.
|
||||
|
||||
A modified version of token replay allows to add or remove tokens when the trace is stuck on the Petri net.
|
||||
These external interventions are tracked and used to compute a fitness score (i.e. degree of conformance).
|
||||
|
||||
Limitations:
|
||||
\begin{itemize}
|
||||
\item Fitness tends to be high for extremely problematic logs.
|
||||
\item If there are too many deviations, the model is flooded with tokens and may result in unexpected behaviors.
|
||||
\item It is a Petri net specific algorithm.
|
||||
\end{itemize}
|
||||
|
||||
\item[Alignment] \marginnote{Alignment}
|
||||
Given a trace $l$ and the reference traces $L_\text{ref}$,
|
||||
alignment is based on the edit distance (i.e. minimum number of modifications) between $l$ and the traces in $L_\text{ref}$.
|
||||
|
||||
The fitness score is based on the lowest and highest edit distances.
|
||||
\end{description}
|
||||
@ -0,0 +1,352 @@
|
||||
\chapter{Description logic}
|
||||
|
||||
|
||||
\section{Syntax}
|
||||
|
||||
\begin{description}
|
||||
\item[Logical symbols] \marginnote{Logical symbols}
|
||||
Symbols with fixed meaning.
|
||||
\begin{description}
|
||||
\item[Punctuation] ( ) [ ]
|
||||
\item[Positive integers]
|
||||
\item[Concept-forming operators] \texttt{ALL}, \texttt{EXISTS}, \texttt{FILLS}, \texttt{AND}
|
||||
\item[Connectives] $\sqsubseteq$, $\doteq$, $\rightarrow$
|
||||
\end{description}
|
||||
|
||||
\item[Non-logical symbols] \marginnote{Non-logical symbols}
|
||||
Domain-dependant symbols.
|
||||
\begin{description}
|
||||
\item[Atomic concepts] Categories (CamelCase, e.g. \texttt{Person}).
|
||||
\item[Roles] Used to describe objects (:CamelCase, e.g. \texttt{:Height}).
|
||||
\item[Constants] (camelCase, e.g. \texttt{johnDoe}).
|
||||
\end{description}
|
||||
|
||||
\item[Complex concept] \marginnote{Complex concept}
|
||||
Concept-forming operators can be used to combine atomic concepts and form complex concepts.
|
||||
A well-formed concept follows the conditions:
|
||||
\begin{itemize}
|
||||
\item An atomic concept is a concept.
|
||||
\item If \texttt{r} is a role and \texttt{d} is a concept, then \texttt{[ALL r d]} is a concept.
|
||||
\item If \texttt{r} is a role and $n$ is a positive integer, then \texttt{[EXISTS $n$ r]} is a concept.
|
||||
\item If \texttt{r} is a role and \texttt{c} is a constant, then \texttt{[FILLS r c]} is a concept.
|
||||
\item If $\texttt{d}_1 \dots \texttt{d}_n$ are concepts,
|
||||
then \texttt{[AND $\texttt{d}_1 \dots \texttt{d}_n$]} is a concept.
|
||||
\end{itemize}
|
||||
|
||||
\item[Sentence] \marginnote{Sentence}
|
||||
Connectives can be used to combine concepts and form sentences.
|
||||
A well-formed sentence follows the conditions:
|
||||
\begin{itemize}
|
||||
\item If $\texttt{d}_1$ and $\texttt{d}_2$ are concepts,
|
||||
then $(\texttt{d}_1 \sqsubseteq \texttt{d}_2)$ is a sentence.
|
||||
\item If $\texttt{d}_1$ and $\texttt{d}_2$ are concepts,
|
||||
then $(\texttt{d}_1 \doteq \texttt{d}_2)$ is a sentence.
|
||||
\item If $\texttt{c}$ is a constant and $\texttt{d}$ is a concept,
|
||||
then $(\texttt{c} \rightarrow \texttt{d})$ is a sentence.
|
||||
\end{itemize}
|
||||
|
||||
\item[Knowledge base] \marginnote{Knowledge base}
|
||||
Collection of sentences.
|
||||
\begin{description}
|
||||
\item[Constants] are individuals of the domain.
|
||||
\item[Concepts] are categories of individuals.
|
||||
\item[Roles] are binary relations between individuals.
|
||||
\end{description}
|
||||
|
||||
|
||||
\item[Assertion box (A-box)] \marginnote{Assertion box (A-box)}
|
||||
List of facts about individuals.
|
||||
|
||||
\item[Terminological box (T-box)] \marginnote{Terminological box (T-box)}
|
||||
List of sentences (axioms) about concepts.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Semantics}
|
||||
|
||||
\subsection{Concept-forming operators}
|
||||
\marginnote{Concept-forming operators}
|
||||
Let \texttt{r} be a role, \texttt{d} be a concept, \texttt{c} be a constant and $n$ a positive integer.
|
||||
The semantics of concept-forming operators are:
|
||||
\begin{descriptionlist}
|
||||
\item[\texttt{[ALL r d]}]
|
||||
Individuals \texttt{r}-related to only individuals of the category \texttt{d}.
|
||||
\begin{example}
|
||||
\texttt{[ALL :HasChild Male]} individuals that have zero children or only male children.
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{[EXISTS $n$ r]}]
|
||||
Individuals \texttt{r}-related to at least $n$ other individuals.
|
||||
\begin{example}
|
||||
\texttt{[EXISTS 1 :Child]} individuals with at least one child.
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{[FILLS r c]}]
|
||||
Individuals \texttt{r}-related to the individual \texttt{c}.
|
||||
\begin{example}
|
||||
\texttt{[FILLS :Child john]} individuals with child \texttt{john}.
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{[AND $\texttt{d}_1 \dots \texttt{d}_n$]}]
|
||||
Individuals belonging to all the categories $\texttt{d}_1 \dots \texttt{d}_n$.
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
\subsection{Sentences}
|
||||
\marginnote{Sentences}
|
||||
Sentences are expressions with truth values in the domain.
|
||||
Let \texttt{d} be a concept and \texttt{c} be a constant.
|
||||
The semantics of sentences are:
|
||||
\begin{descriptionlist}
|
||||
\item[$\texttt{d}_1 \sqsubseteq \texttt{d}_2$]
|
||||
Concept $\texttt{d}_1$ is subsumed by $\texttt{d}_2$.
|
||||
\begin{example}
|
||||
$\texttt{PhDStudent} \sqsubseteq \texttt{Student}$ as every PhD is also a student.
|
||||
\end{example}
|
||||
|
||||
\item[$\texttt{d}_1 \doteq \texttt{d}_2$]
|
||||
Concept $\texttt{d}_1$ is equivalent to $\texttt{d}_2$.
|
||||
\begin{example}
|
||||
$\texttt{PhDStudent} \doteq \texttt{[AND Student :Graduated :HasFunding]}$
|
||||
\end{example}
|
||||
|
||||
\item[$\texttt{c} \rightarrow \texttt{d}$]
|
||||
The individual \texttt{c} satisfies the description of the concept \texttt{d}.
|
||||
\begin{example}
|
||||
$\texttt{federico} \rightarrow \texttt{Professor}$
|
||||
\end{example}
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
\subsection{Interpretation}
|
||||
|
||||
\begin{description}
|
||||
\item[Interpretation] \marginnote{Interpretation}
|
||||
An interpretation $\mathfrak{I}$ in description logic is a pair ($\mathcal{D}, \mathcal{I}$) where:
|
||||
\begin{itemize}
|
||||
\item $\mathcal{D}$ is the domain.
|
||||
\item $\mathcal{I}$ is the interpretation mapping.
|
||||
\begin{description}
|
||||
\item[Constant]
|
||||
Let \texttt{c} be a constant, $\mathcal{I}[\texttt{c}] \in \mathcal{D}$.
|
||||
\item[Atomic concept]
|
||||
Let \texttt{a} be an atomic concept, $\mathcal{I}[\texttt{a}] \subseteq \mathcal{D}$.
|
||||
\item[Role]
|
||||
Let \texttt{r} be a role, $\mathcal{I}[\texttt{r}] \subseteq \mathcal{D} \times \mathcal{D}$.
|
||||
\item[\texttt{Thing}]
|
||||
The concept \texttt{Thing} corresponds to the domain: $\mathcal{I}[\texttt{Thing}] = \mathcal{D}$.
|
||||
\item[\texttt{[ALL r d]}]
|
||||
\[
|
||||
\mathcal{I}[\texttt{[ALL r d]}] =
|
||||
\{ \texttt{x} \in \mathcal{D} \mid \forall \texttt{y}:
|
||||
\langle \texttt{x}, \texttt{y} \rangle \in \mathcal{I}[\texttt{r}] \text{ then } \texttt{y} \in \mathcal{I}[\texttt{d}] \}
|
||||
\]
|
||||
\item[\texttt{[EXISTS $n$ r]}]
|
||||
\[
|
||||
\mathcal{I}[\texttt{[EXISTS $n$ r]}] =
|
||||
\{ \texttt{x} \in \mathcal{D} \mid \text{ exists at least $n$ distinct } \texttt{y}:
|
||||
\langle \texttt{x}, \texttt{y} \rangle \in \mathcal{I}[\texttt{r}] \}
|
||||
\]
|
||||
\item[\texttt{[FILLS r c]}]
|
||||
\[
|
||||
\mathcal{I}[\texttt{[FILLS r c]}] = \{ \texttt{x} \in \mathcal{D} \mid
|
||||
\langle \texttt{x}, \mathcal{I}[\texttt{c}] \rangle \in \mathcal{I}[\texttt{r}] \}
|
||||
\]
|
||||
\item[\texttt{[AND $\texttt{d}_1 \dots \texttt{d}_n$]}]
|
||||
\[
|
||||
\mathcal{I}[\texttt{[AND $\texttt{d}_1 \dots \texttt{d}_n$]}] =
|
||||
\mathcal{I}[\texttt{d}_1] \cap \dots \cap \mathcal{I}[\texttt{d}_n]
|
||||
\]
|
||||
\end{description}
|
||||
\end{itemize}
|
||||
|
||||
\item[Model] \marginnote{Model}
|
||||
Given an interpretation $\mathfrak{I} = (\mathcal{D}, \mathcal{I})$,
|
||||
a sentence is true under $\mathfrak{I}$ ($\mathfrak{I} \models \text{sentence}$) if:
|
||||
\begin{itemize}
|
||||
\item $\mathfrak{I} \models (\texttt{c} \rightarrow \texttt{d})$ iff $\mathcal{I}[\texttt{c}] \in \mathcal{I}[\texttt{d}]$.
|
||||
\item $\mathfrak{I} \models (\texttt{d}_\texttt{1} \sqsubseteq \texttt{d}_\texttt{2})$ iff
|
||||
$\mathcal{I}[\texttt{d}_\texttt{1}] \subseteq \mathcal{I}[\texttt{d}_\texttt{2}]$.
|
||||
\item $\mathfrak{I} \models (\texttt{d}_\texttt{1} \doteq \texttt{d}_\texttt{2})$ iff
|
||||
$\mathcal{I}[\texttt{d}_\texttt{1}] = \mathcal{I}[\texttt{d}_\texttt{2}]$.
|
||||
\end{itemize}
|
||||
|
||||
Given a set of sentences $S$, $\mathfrak{I}$ models $S$ if $\mathfrak{I} \models S$.
|
||||
|
||||
\item[Entailment] \marginnote{Entailment}
|
||||
A set of sentences $S$ logically entails a sentence $\alpha$ if:
|
||||
\[ \forall \mathfrak{I}:\, (\mathfrak{I} \models S) \rightarrow (\mathfrak{I} \models \alpha) \]
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Reasoning}
|
||||
|
||||
\subsection{T-box reasoning}
|
||||
|
||||
Given a knowledge base of a set of sentences $S$, we would like to be able to determine the following:
|
||||
\begin{descriptionlist}
|
||||
\item[Satisfiability] \marginnote{Satisfiability}
|
||||
A concept \texttt{d} is satisfiable w.r.t. $S$ if:
|
||||
\[ \exists \mathfrak{I}, (\mathfrak{I} \models S): \mathcal{I}[\texttt{d}] \neq \varnothing \]
|
||||
|
||||
\item[Subsumption] \marginnote{Subsumption}
|
||||
A concept $\texttt{d}_1$ is subsumed by $\texttt{d}_2$ w.r.t. $S$ if:
|
||||
\[ \forall \mathfrak{I}, (\mathfrak{I} \models S): \mathcal{I}[\texttt{d}_1] \subseteq \mathcal{I}[\texttt{d}_2] \]
|
||||
|
||||
\item[Equivalence] \marginnote{Equivalence}
|
||||
A concept $\texttt{d}_1$ is equivalent to $\texttt{d}_2$ w.r.t. $S$ if:
|
||||
\[ \forall \mathfrak{I}, (\mathfrak{I} \models S): \mathcal{I}[\texttt{d}_1] = \mathcal{I}[\texttt{d}_2] \]
|
||||
|
||||
\item[Disjointness] \marginnote{Disjointness}
|
||||
A concept $\texttt{d}_1$ is disjoint to $\texttt{d}_2$ w.r.t. $S$ if:
|
||||
\[ \forall \mathfrak{I}, (\mathfrak{I} \models S): \mathcal{I}[\texttt{d}_1] \neq \mathcal{I}[\texttt{d}_2] \]
|
||||
\end{descriptionlist}
|
||||
|
||||
\begin{theorem}[Reduction to subsumption]
|
||||
\marginnote{Reduction to subsumption}
|
||||
Given the concepts $\texttt{d}_1$ and $\texttt{d}_2$, it holds that:
|
||||
\begin{itemize}
|
||||
\item $\texttt{d}_1 \text{ is unsatisfiable } \iff \texttt{d}_1 \sqsubseteq \bot$.
|
||||
\item $\texttt{d}_1 \doteq \texttt{d}_2 \iff \texttt{d}_1 \sqsubseteq \texttt{d}_2 \land \texttt{d}_2 \sqsubseteq \texttt{d}_1$.
|
||||
\item $\texttt{d}_1 \text{ and } \texttt{d}_2 \text{ are disjoint} \iff (\texttt{d}_1 \cap \texttt{d}_2) \sqsubseteq \bot$.
|
||||
\end{itemize}
|
||||
\end{theorem}
|
||||
|
||||
\subsection{A-box reasoning}
|
||||
Given a constant \texttt{c}, a concept \texttt{d} and a set of sentences $S$, we can determine the following:
|
||||
\begin{descriptionlist}
|
||||
\item[Satisfiability] \marginnote{Satisfiability}
|
||||
A constant \texttt{c} satisfies the concept \texttt{d} if:
|
||||
\[ S \models (\texttt{c} \rightarrow \texttt{d}) \]
|
||||
|
||||
Note that it can be reduced to subsumption.
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
\subsection{Computing subsumptions}
|
||||
|
||||
Given a knowledge base $KB$ and two concepts \texttt{d} and \texttt{e},
|
||||
we want to prove:
|
||||
\[ KB \models (\texttt{d} \sqsubseteq \texttt{e}) \]
|
||||
The following algorithms can be employed:
|
||||
\begin{descriptionlist}
|
||||
\item[Structural matching] \marginnote{Structural matching}
|
||||
\phantom{}
|
||||
\begin{enumerate}
|
||||
\item Normalize \texttt{d} and \texttt{e} into a conjunctive form:
|
||||
\[ \texttt{d} = \texttt{[AND d$_1$ \dots d$_n$]} \hspace*{1cm} \texttt{e} = \texttt{[AND e$_1$ \dots e$_m$]} \]
|
||||
\item Check if each part of \texttt{d} is accounted by at least a component of \texttt{e}.
|
||||
\end{enumerate}
|
||||
|
||||
\item[Tableaux-based algorithms] \marginnote{Tableaux-based algorithms}
|
||||
Exploit the following theorem:
|
||||
\[ \big( KB \models (\texttt{d} \sqsubseteq \texttt{e}) \big) \iff
|
||||
\big( KB \cup (x : \texttt{[AND d $\lnot$e]}) \big) \text{ is inconsistent} \]
|
||||
|
||||
Note: similar to refutation.
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
\subsection{Open-world assumption}
|
||||
|
||||
\begin{description}
|
||||
\item[Open-world assumption] \marginnote{Open-world assumption}
|
||||
If a sentence cannot be inferred, its truth value is unknown.
|
||||
\end{description}
|
||||
|
||||
Description logics are based on the open-world assumption.
|
||||
To reason in open-world assumption, all the possible models are split upon encountering unknown facts
|
||||
depending on the possible cases (Oedipus example).
|
||||
|
||||
|
||||
|
||||
\section{Expanding description logic}
|
||||
It is possible to expand a description logic by:
|
||||
\begin{descriptionlist}
|
||||
\item[Adding concept-forming operators] \marginnote{Adding concept-forming operators}
|
||||
Let \texttt{r} be a role, \texttt{d} be a concept, \texttt{c} be a constant and $n$ a positive integer.
|
||||
We can extend our description logic with:
|
||||
\begin{description}
|
||||
\item[\texttt{[AT-MOST $n$ r]}]
|
||||
Individuals \texttt{r}-related to at most $n$ other individuals.
|
||||
\begin{example}
|
||||
\texttt{[AT-MOST $1$ :Child]} individuals with only a child.
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{[ONE-OF c$_1$ $\dots$ c$_n$]}]
|
||||
Concept only satisfied by \texttt{c$_1$ $\dots$ c$_n$}.
|
||||
\begin{example}
|
||||
$\texttt{Beatles} \doteq \texttt{[ALL :BandMember [ONE-OF john paul george ringo]]}$
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{[EXISTS $n$ r d]}]
|
||||
Individuals \texttt{r}-related to at least $n$ individuals in the category \texttt{d}.
|
||||
\begin{example}
|
||||
\texttt{[EXISTS $2$ :Child Male]} individuals with at least two male children.
|
||||
\end{example}
|
||||
Note: this increases the computational complexity of entailment.
|
||||
\end{description}
|
||||
|
||||
\item[Relating roles] \marginnote{Relating roles}
|
||||
\begin{description}
|
||||
\item[\texttt{[SAME-AS r$_1$ r$_2$]}]
|
||||
Equates fillers of the roles r$_1$ and r$_2$
|
||||
\begin{example}
|
||||
\texttt{[SAME-AS :CEO :Owner]}
|
||||
\end{example}
|
||||
Note: this increases the computational complexity of entailment.
|
||||
Role chaining also leads to undecidability.
|
||||
\end{description}
|
||||
|
||||
\item[Adding rules] \marginnote{Adding rules}
|
||||
Rules are useful to add conditions (e.g. \texttt{if d$_1$ then [FILLS r c]}).
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
\section{Description logics family}
|
||||
|
||||
Depending on the number of operators, a description logic can be:
|
||||
\begin{itemize}
|
||||
\item More expressive.
|
||||
\item Computationally more expensive.
|
||||
\item Undecidable.
|
||||
\end{itemize}
|
||||
|
||||
\begin{description}
|
||||
\item[Attributive language ($\mathcal{AL}$)]
|
||||
Minimal description logic with:
|
||||
\begin{itemize}
|
||||
\item Atomic concepts.
|
||||
\item Universal concept (\texttt{Thing} or $\top$).
|
||||
\item Bottom concept (\texttt{Nothing} or $\bot$).
|
||||
\item Atomic negation (only for atomic concepts).
|
||||
\item \texttt{AND} operator ($\sqcap$).
|
||||
\item \texttt{ALL} operator ($\forall$).
|
||||
\item \texttt{[EXISTS $1$ r]} operator ($\exists$).
|
||||
\end{itemize}
|
||||
|
||||
\item[Attributive language complement ($\mathcal{ALC}$)]
|
||||
$\mathcal{AL}$ with negation for concepts.
|
||||
\end{description}
|
||||
|
||||
\begin{table}[h]
|
||||
\centering
|
||||
\begin{tabular}{|c|c|}
|
||||
\hline
|
||||
$\mathcal{F}$ & Functional properties \\ \hline
|
||||
$\mathcal{E}$ & Full existential quantification \\ \hline
|
||||
$\mathcal{U}$ & Concept union \\ \hline
|
||||
$\mathcal{C}$ & Complex concept negation \\ \hline
|
||||
$\mathcal{S}$ & $\mathcal{ALC}$ with transitive roles \\ \hline
|
||||
$\mathcal{H}$ & Role hierarchy \\ \hline
|
||||
$\mathcal{R}$ & \makecell[c]{Limited complex roles axioms\\Reflexivity and irreflexivity\\Roles disjointness} \\ \hline
|
||||
$\mathcal{O}$ & Nominals \\ \hline
|
||||
$\mathcal{I}$ & Inverse properties \\ \hline
|
||||
$\mathcal{N}$ & Cardinality restrictions \\ \hline
|
||||
$\mathcal{Q}$ & Qualified cardinality restrictions \\ \hline
|
||||
$\mathcal{(D)}$ & Datatype properties, data values and data types \\ \hline
|
||||
\end{tabular}
|
||||
\caption{Name and expressivity of logics}
|
||||
\end{table}
|
||||
@ -0,0 +1,192 @@
|
||||
\chapter{Forward reasoning}
|
||||
|
||||
\begin{description}
|
||||
\item[Logical implication] \marginnote{Logical implication}
|
||||
Simplest form of rule:
|
||||
\[ p_1, \dots, p_n \Rightarrow q_1, \dots, q_m \]
|
||||
where:
|
||||
\begin{descriptionlist}
|
||||
\item[Left hand side (LHS)] $p_1, \dots, p_n$
|
||||
\item[Right hand side (RHS)] $q_1, \dots, q_m$
|
||||
\end{descriptionlist}
|
||||
|
||||
\item[Modus ponens] \marginnote{Modus ponens}
|
||||
If $A$ and $A \Rightarrow B$ are true, then we can derive that $B$ is true.
|
||||
|
||||
\item[Production rules] \marginnote{Production rules}
|
||||
Approach that allows to dynamically add facts to the knowledge base (differently from backward reasoning in Prolog).
|
||||
|
||||
When a fact is added, the reasoning mechanism is triggered:
|
||||
\begin{descriptionlist}
|
||||
\item[Match] Search for the rules whose LHS match the fact and (arbitrarily) decide which to trigger.
|
||||
\item[Conflict resolution] Triggered rules are put in an agenda where conflicts are solved.
|
||||
\item[Execution] The RHS of the triggered rules are executed and the effects are performed.
|
||||
The knowledge base is updated with the (copies of the) new facts.
|
||||
\end{descriptionlist}
|
||||
These steps are executed until quiescence as the execution step may add new facts.
|
||||
|
||||
\item[Working memory] \marginnote{Working memory}
|
||||
Data structure that contains the currently valid set of facts and rules.
|
||||
|
||||
The performance of a production rules system depends on the efficiency of the working memory.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{RETE algorithm}
|
||||
|
||||
RETE is an efficient algorithm for implementing rule-based systems.
|
||||
|
||||
\subsection{Match}
|
||||
\begin{description}
|
||||
\item[Pattern] \marginnote{Pattern}
|
||||
The LHS of a rule is expressed as a conjunction of patterns (conditions).
|
||||
|
||||
A pattern can test:
|
||||
\begin{descriptionlist}
|
||||
\item[Intra-element features] Features that can be tested directly on a fact.
|
||||
\item[Inter-element features] Features that involve more facts.
|
||||
\end{descriptionlist}
|
||||
|
||||
\item[Conflict set] \marginnote{Conflict set}
|
||||
Set of all possible instantiations of production rules.
|
||||
Each rule is described as:
|
||||
\[ \langle \text{Rule}, \text{ list of facts matched by its LHS} \rangle \]
|
||||
|
||||
Instead of naively checking a rule over all the facts, each rule has associated the facts that match its LHS patterns.
|
||||
|
||||
\item[LHS network]
|
||||
Compile the LHSs into networks:
|
||||
\begin{descriptionlist}
|
||||
\item[Alpha-network] \marginnote{Alpha-network}
|
||||
For intra-element features.
|
||||
The outcome is stored in alpha-memories and used by the beta network.
|
||||
|
||||
\item[Beta-network] \marginnote{Beta-network}
|
||||
For inter-element features.
|
||||
The outcome is stored in beta-memories and corresponds to the conflict set.
|
||||
\end{descriptionlist}
|
||||
If more rules use the same pattern, the node of that pattern is reused and possibly outputting to different memories.
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Conflict resolution}
|
||||
RETE allows different strategies to handle conflicts:
|
||||
\begin{itemize}
|
||||
\item Rule priority.
|
||||
\item Rule ordering.
|
||||
\item Temporal attributes.
|
||||
\item Rule complexity.
|
||||
\end{itemize}
|
||||
The best approach depends on the use case.
|
||||
|
||||
|
||||
\subsection{Execution}
|
||||
By default, RETE executes all the rules in the agenda and
|
||||
then checks for possible side effects that modify the working memory in a second moment.
|
||||
|
||||
Note that it is very easy to create loops.
|
||||
|
||||
|
||||
|
||||
\section{Drools framework}
|
||||
\marginnote{Drools}
|
||||
|
||||
RETE-based rule engine that uses Java.
|
||||
|
||||
\begin{description}
|
||||
\item[Rule] A rule has structure:
|
||||
\begin{lstlisting}[language={java}]
|
||||
rule "rule name"
|
||||
// Rule attributes
|
||||
when
|
||||
// LHS
|
||||
then
|
||||
// RHS
|
||||
end
|
||||
\end{lstlisting}
|
||||
|
||||
\item[Quantifiers] \phantom{}
|
||||
\begin{description}
|
||||
\item[\texttt{exists P(...)}]
|
||||
Trigger the rule once if at least a fact \texttt{P(...)} exists in the working memory.
|
||||
\item[\texttt{forall P(...)}]
|
||||
Trigger the rule if all the instances of \texttt{P(...)} match.
|
||||
The rule can be executed multiple times.
|
||||
\item[\texttt{not P(...)}]
|
||||
Trigger the rule if the fact \texttt{P(...)} does not exist in the working memory.
|
||||
Note that a negation in different positions might result in different behaviors.
|
||||
\end{description}
|
||||
|
||||
\item[Consequences]
|
||||
Drools allows two types of RHS operations:
|
||||
\begin{description}
|
||||
\item[Logic] \phantom{}
|
||||
\begin{description}
|
||||
\item[Insert]
|
||||
Create a new fact and insert it in the working memory.
|
||||
Existing rules may trigger if they match the new fact.
|
||||
|
||||
If the conditions of the rule that inserted a fact are no longer true, the inserted fact is automatically retracted.
|
||||
|
||||
\item[Retract] Remove a fact from the working memory.
|
||||
|
||||
\item[Modify]
|
||||
A combination of retract and insert executed consecutively.
|
||||
The \texttt{no-loop} keyword can be used to avoid loops.
|
||||
\end{description}
|
||||
|
||||
\item[Non-logic]
|
||||
Execution of Java code or external side effects.
|
||||
\end{description}
|
||||
|
||||
\item[Conflict resolution] \phantom{}
|
||||
\begin{description}
|
||||
\item[Salience score]
|
||||
\item[Agenda group]
|
||||
Associate a group to each rule. The method \texttt{setFocus} can be used to prioritize certain groups.
|
||||
\item[Activation group]
|
||||
Only one rule among the ones with the same activation group is executed (i.e. mutual exclusion).
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Complex event processing}
|
||||
|
||||
\begin{description}
|
||||
\item[Event] \marginnote{Event}
|
||||
Information with a description and temporal information (instantaneous or with a duration).
|
||||
|
||||
\item[Simple event] \marginnote{Simple event}
|
||||
Event detected outside an event processing system (e.g. a sensor). It does not provide any information alone.
|
||||
|
||||
\item[Complex event] \marginnote{Complex event}
|
||||
Event generated by an event processing system and able to provides a higher informative payload.
|
||||
|
||||
\item[Complex event processing (CEP)] \marginnote{Complex event processing}
|
||||
Paradigm for dealing with a large amount of information.
|
||||
Takes as input different types of events and outputs durative events.
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Drools}
|
||||
|
||||
Drools supports CEP by representing events as facts.
|
||||
|
||||
\begin{description}
|
||||
\item[Clock]
|
||||
Mechanism to specify time conditions to reason over temporal intervals.
|
||||
|
||||
\item[Sliding windows] \phantom{}
|
||||
\begin{description}
|
||||
\item[Time-based window] Select events within a time slice.
|
||||
\item[Length-based window] Select the last $n$ events.
|
||||
\end{description}
|
||||
|
||||
\item[Expiration]
|
||||
Mechanism to specify an expiration time for events and discard them from the working memory.
|
||||
|
||||
\item[Temporal reasoning]
|
||||
Allen's temporal operators for temporal reasoning.
|
||||
\end{description}
|
||||
@ -0,0 +1,12 @@
|
||||
\newpage
|
||||
\lohead{\color{gray} Chapter taken from \href{\gitLAAITwo}{\texttt{\color{gray}Languages and Algorithms for AI (module 2)}}}
|
||||
\lehead{\color{gray} Chapter taken from \href{\gitLAAITwo}{\texttt{\color{gray}Languages and Algorithms for AI (module 2)}}}
|
||||
|
||||
\graphicspath{{../../languages-and-algorithms-for-ai/module2/}}
|
||||
\input{../../languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex}
|
||||
\input{../../languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex}
|
||||
\graphicspath{}
|
||||
|
||||
\newpage
|
||||
\lohead{}
|
||||
\lehead{}
|
||||
@ -0,0 +1,263 @@
|
||||
\chapter{Ontologies}
|
||||
|
||||
\begin{description}
|
||||
\item[Ontology] \marginnote{Ontology}
|
||||
Formal (non-ambiguous) and explicit (obtainable through a finite sound procedure)
|
||||
description of a domain.
|
||||
|
||||
\item[Category] \marginnote{Category}
|
||||
Can be organized hierarchically on different levels of generality.
|
||||
|
||||
\item[Object] \marginnote{Object}
|
||||
Belongs to one or more categories.
|
||||
|
||||
\item[Upper/general ontology] \marginnote{Upper/general ontology}
|
||||
Ontology focused on the most general domain.
|
||||
|
||||
Properties:
|
||||
\begin{itemize}
|
||||
\item Should be applicable to almost any special domain.
|
||||
\item Combining general concepts should not incur in inconsistencies.
|
||||
\end{itemize}
|
||||
|
||||
Approaches to create ontologies:
|
||||
\begin{itemize}
|
||||
\item Created by philosophers/logicians/researchers.
|
||||
\item Automatic knowledge extraction from well-structured databases.
|
||||
\item Created from text documents (e.g. web).
|
||||
\item Crowd-sharing information.
|
||||
\end{itemize}
|
||||
\end{description}
|
||||
|
||||
|
||||
\section{Categories}
|
||||
\begin{description}
|
||||
\item[Category] \marginnote{Category}
|
||||
Used in human reasoning when the goal is category-driven (in contrast to specific-instance-driven).
|
||||
|
||||
In first-order logic, categories can be represented through:
|
||||
\begin{descriptionlist}
|
||||
\item[Predicate] \marginnote{Predicate categories}
|
||||
A predicate to tell if an object belongs to a category
|
||||
(e.g. \texttt{Car(c1)} indicates that \texttt{c1} is a car).
|
||||
|
||||
\item[Reification] \marginnote{Reification}
|
||||
Represent categories as objects as well (e.g. $\texttt{c1} \in \texttt{Car}$).
|
||||
\end{descriptionlist}
|
||||
\end{description}
|
||||
|
||||
\subsection{Reification properties and operations}
|
||||
\begin{description}
|
||||
\item[Membership] \marginnote{Membership}
|
||||
Indicates if an object belongs to a category.
|
||||
(e.g. $\texttt{c1} \in \texttt{Car}$).
|
||||
|
||||
\item[Subclass] \marginnote{Subclass}
|
||||
Indicates if a category is a subcategory of another one.
|
||||
(e.g. $\texttt{Car} \subset \texttt{Vehicle}$).
|
||||
|
||||
\item[Necessity] \marginnote{Necessity}
|
||||
Members of a category enjoy some properties
|
||||
(e.g. $(\text{x} \in \texttt{Car}) \Rightarrow \texttt{hasWheels(x)}$).
|
||||
|
||||
\item[Sufficiency] \marginnote{Sufficiency}
|
||||
Sufficient conditions to be part of a category\\
|
||||
(e.g. $\texttt{hasPlate(x)} \land \texttt{hasWheels(x)} \Rightarrow \texttt{x} \in \texttt{Car}$).
|
||||
|
||||
\item[Category-level properties] \marginnote{Category-level properties}
|
||||
Category themselves can enjoy properties\\
|
||||
(e.g. $\texttt{Car} \in \texttt{VehicleType}$)
|
||||
|
||||
\item[Disjointness] \marginnote{Disjointness}
|
||||
Given a set of categories $S$, the categories in $S$ are disjoint iff they all have different objects:
|
||||
\[ \texttt{disjoint($S$)} \iff (\forall c_1, c_2 \in S, c_1 \neq c_2 \Rightarrow c_1 \cap c_2 = \emptyset) \]
|
||||
|
||||
\item[Exhaustive decomposition] \marginnote{Exhaustive decomposition}
|
||||
Given a category $c$ and a set of categories $S$, $S$ is an exhaustive decomposition of $c$ iff
|
||||
any element in $c$ belongs to at least a category in $S$:
|
||||
\[ \texttt{exhaustiveDecomposition($S$, $c$)} \iff \forall o: (o \in c \iff \exists c_2 \in S: o \in c_2) \]
|
||||
|
||||
\item[Partition] \marginnote{Partition}
|
||||
Given a category $c$ and a set of categories $S$, $S$ is a partition of $c$ when:
|
||||
\[ \texttt{partition($S$, $c$)} \iff \texttt{disjoint($S$)} \land \texttt{exhaustiveDecomposition($S$, $c$)} \]
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Physical composition}
|
||||
Objects (meronyms) are part of a whole (holonym).
|
||||
|
||||
\begin{description}
|
||||
\item[Part-of] \marginnote{Part-of}
|
||||
If the objects have a structural relation (e.g. $\texttt{partOf(cylinder1, engine1)}$).
|
||||
|
||||
Properties:
|
||||
\begin{descriptionlist}
|
||||
\item[Transitivity] $\texttt{partOf(x, y)} \land \texttt{partOf(y, z)} \Rightarrow \texttt{partOf(x, z)}$
|
||||
\item[Reflexivity] $\texttt{partOf(x, x)}$
|
||||
\end{descriptionlist}
|
||||
|
||||
\item[Bunch-of] \marginnote{Bunch-of}
|
||||
If the objects do not have a structural relation.
|
||||
Useful to define a composition of countable objects
|
||||
(e.g. $\texttt{bunchOf({nail1, nail3, nail4})}$).
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Measures}
|
||||
|
||||
A property of objects.
|
||||
|
||||
\begin{description}
|
||||
\item[Quantitative measure] \marginnote{Quantitative measure}
|
||||
Something that can be measured using a unit\\
|
||||
(e.g. $\texttt{length(table1)} = \texttt{cm(80)}$).
|
||||
|
||||
Qualitative measures propagate when using \texttt{partOf} or \texttt{bunchOf}
|
||||
(e.g. the weight of a car is the sum of its parts).
|
||||
|
||||
\item[Qualitative measure] \marginnote{Qualitative measure}
|
||||
Something that can be measured using terms with a partial or total order relation
|
||||
(e.g. $\{ \texttt{good}, \texttt{neutral}, \texttt{bad} \}$).
|
||||
|
||||
Qualitative measures do not propagate when using \texttt{partOf} or \texttt{bunchOf}.
|
||||
|
||||
\item[Fuzzy logic] \marginnote{Fuzzy logic}
|
||||
Provides a semantics to qualitative measures (i.e. convert qualitative to quantitative).
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection{Things vs stuff}
|
||||
|
||||
\begin{description}
|
||||
\item[Intrinsic property] \marginnote{Intrinsic property}
|
||||
Related to the substance of the object. It is retained when the object is divided
|
||||
(e.g. water boils at 100°C).
|
||||
|
||||
\item[Extrinsic property] \marginnote{Extrinsic property}
|
||||
Related to the structure of the object. It is not retained when the object is divided
|
||||
(e.g. the weight of an object changes when split).
|
||||
|
||||
\item[Substance] \marginnote{Substance}
|
||||
Category of objects with only intrinsic properties.
|
||||
|
||||
\begin{description}
|
||||
\item[Stuff] \marginnote{Stuff}
|
||||
The most general substance category.
|
||||
\end{description}
|
||||
|
||||
\item[Count noun] \marginnote{Count noun}
|
||||
Category of objects with only extrinsic properties.
|
||||
|
||||
\begin{description}
|
||||
\item[Things] \marginnote{Things}
|
||||
The most general object category.
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Semantic networks}
|
||||
\marginnote{Semantic networks}
|
||||
Graphical representation of objects and categories connected through labeled links.
|
||||
|
||||
\begin{figure}[h]
|
||||
\centering
|
||||
\includegraphics[width=0.4\textwidth]{img/semantic_network.png}
|
||||
\caption{Example of semantic network}
|
||||
\end{figure}
|
||||
|
||||
\begin{description}
|
||||
\item[Objects and categories] Represented using the same symbol.
|
||||
|
||||
\item[Links] Four different types of links:
|
||||
\begin{itemize}
|
||||
\item Relation between objects (e.g. \texttt{SisterOf}).
|
||||
\item Property of a category (e.g. 2 \texttt{Legs}).
|
||||
\item Is-a relation (e.g. \texttt{SubsetOf}).
|
||||
\item Property of the members of a category (e.g. \texttt{HasMother}).
|
||||
\end{itemize}
|
||||
\end{description}
|
||||
|
||||
\begin{description}
|
||||
\item[Single inheritance reasoning] \marginnote{Single inheritance reasoning}
|
||||
Starting from an object, check if it has the queried property.
|
||||
If not, iteratively move up to the category it belongs to and check for the property.
|
||||
|
||||
\item[Multiple inheritance reasoning] \marginnote{Multiple inheritance reasoning}
|
||||
Reasoning is not possible as it is not clear which parent to choose.
|
||||
\end{description}
|
||||
|
||||
\begin{description}
|
||||
\item[Limitations]
|
||||
Compared to first-order logic, semantic networks do not have:
|
||||
\begin{itemize}
|
||||
\item Negations.
|
||||
\item Universally and existentially quantified properties.
|
||||
\item Disjunctions.
|
||||
\item Nested function symbols.
|
||||
\end{itemize}
|
||||
|
||||
Many semantic network systems allow to attach special procedures to handle special cases
|
||||
that the standard inference algorithm cannot handle.
|
||||
This approach is powerful but does not have a corresponding logical meaning.
|
||||
|
||||
\item[Advantages]
|
||||
With semantic networks, it is easy to attach default properties to categories and
|
||||
override them on the objects (i.e. \texttt{Legs} of \texttt{John}).
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Frames}
|
||||
\marginnote{Frames}
|
||||
Knowledge that describes an object in terms of its properties.
|
||||
Each frame has:
|
||||
\begin{itemize}
|
||||
\item A unique name
|
||||
\item Properties represented as pairs \texttt{<slot - filler>}
|
||||
\end{itemize}
|
||||
|
||||
\begin{example}
|
||||
\phantom{}\\[-1em]
|
||||
\begin{lstlisting}[mathescape=true, language={}]
|
||||
(
|
||||
toronto
|
||||
<:Instance-Of City>
|
||||
<:Province ontario>
|
||||
<:Population 4.5M>
|
||||
)
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
\begin{description}
|
||||
\item[Prototype] \marginnote{Prototype}
|
||||
Members of a category used as comparison metric to determine if another object belongs to the same class
|
||||
(i.e. an object belongs to a category if it is similar enough to the prototypes of that category).
|
||||
|
||||
\item[Defeasible value] \marginnote{Defeasible value}
|
||||
Value that is allowed to be different when comparing an object to a prototype.
|
||||
|
||||
\item[Facets] \marginnote{Facets}
|
||||
Additional information contained in a slot for its filler (e.g. default value, type, domain).
|
||||
|
||||
\begin{description}
|
||||
\item[Procedural information]
|
||||
Fillers can be a procedure that can be activated by specific facets:
|
||||
\begin{descriptionlist}
|
||||
\item[\texttt{if-needed}] Looks for the value of the slot.
|
||||
\item[\texttt{if-added}] Adds a value.
|
||||
\item[\texttt{if-removed}] Removes a value.
|
||||
\end{descriptionlist}
|
||||
\begin{example}
|
||||
\phantom{}\\[-1em]
|
||||
\begin{lstlisting}[mathescape=true, language={}]
|
||||
(
|
||||
toronto
|
||||
<:Instance-Of City>
|
||||
<:Province ontario>
|
||||
<:Population [if-needed QueryDB]>
|
||||
)
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
\end{description}
|
||||
\end{description}
|
||||
@ -0,0 +1,94 @@
|
||||
\chapter{Probabilistic logic reasoning}
|
||||
|
||||
\begin{description}
|
||||
\item[Probabilistic logic programming] \marginnote{Probabilistic logic programming}
|
||||
Adds probability distributions over logic programs allowing to define different worlds.
|
||||
Joint distributions can also be defined over worlds and allow to answer to queries.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Logic programs with annotated disjunctions (LPAD)}
|
||||
\marginnote{LPAD}
|
||||
|
||||
\subsection{Syntax}
|
||||
|
||||
\begin{description}
|
||||
\item[\texttt{null}]
|
||||
Atom that can only appear in the head of a clause and
|
||||
cancels the clause (i.e. equivalent of not having the clause).
|
||||
\end{description}
|
||||
|
||||
The head of each clause is defined as a disjunction of atoms, each with a probability.
|
||||
More specifically, each clause has a probability distribution over its head.
|
||||
|
||||
\begin{example}
|
||||
\phantom{}
|
||||
\begin{lstlisting}
|
||||
sneezing(X):0.7 ; null:0.3 :- flu(X).
|
||||
sneezing(X):0.8 ; null:0.2 :- hay_fever(X).
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
|
||||
\subsection{Distribution semantics}
|
||||
|
||||
\begin{description}
|
||||
\item[Worlds] \marginnote{World}
|
||||
Given a clause $C$ and a substitution $\theta$ such that $C\theta$ is ground,
|
||||
the following operations are defined for LPAD:
|
||||
\begin{descriptionlist}
|
||||
\item[Atomic choice] \marginnote{Atomic choice}
|
||||
An atomic choice $(C, \theta, i)$ is the selection of the $i$-th atom in the head of $C$ for grounding.
|
||||
|
||||
\item[Composite choice] \marginnote{Composite choice}
|
||||
A composite choice $\kappa$ is a set of atomic choices.
|
||||
The probability of a composite choice is the following:
|
||||
\[ \prob{\kappa} = \prod_{(C, \theta, i) \in \kappa} \prob{C, i} \]
|
||||
where $\prob{C, i}$ is the probability of choosing the $i$-th atom in the head of $C$.
|
||||
|
||||
\item[Selection] \marginnote{Selection}
|
||||
A selection $\sigma$ is a composite choice where an atom from the head of each clause for each grounding has been chosen.
|
||||
In other words, a selection can be defined only when the program is ground.
|
||||
|
||||
A selection $\sigma$ identifies a world $w_\sigma$ and has probability:
|
||||
\[ \prob{w_\sigma} = \prob{\sigma} = \prod_{(C, \theta, i) \in \sigma} \prob{C, i} \]
|
||||
\end{descriptionlist}
|
||||
|
||||
\begin{example}
|
||||
Given the program:
|
||||
\begin{lstlisting}
|
||||
sneezing(X):0.7 ; null:0.3 :- flu(X).
|
||||
sneezing(X):0.8 ; null:0.2 :- hay_fever(X).
|
||||
\end{lstlisting}
|
||||
|
||||
The possible worlds are:
|
||||
\begin{center}
|
||||
\includegraphics[width=0.7\textwidth]{img/_probabilistic_logic_example.pdf}
|
||||
\end{center}
|
||||
\end{example}
|
||||
|
||||
\item[Queries] \marginnote{Queries}
|
||||
Given a ground query $Q$ and a world $w$, the probability of $Q$ being true in $w$ is trivially:
|
||||
\[
|
||||
\prob{Q \mid w} =
|
||||
\begin{cases}
|
||||
1 & \text{ if $Q$ is true in $w$}\\
|
||||
0 & \text{ otherwise}
|
||||
\end{cases}
|
||||
\]
|
||||
|
||||
The overall probability of $Q$ is:
|
||||
\[ \prob{Q} = \sum_w \prob{Q, w} = \sum_w \prob{Q \mid w}\prob{w} = \sum_{w \models Q} \prob{w} \]
|
||||
|
||||
\begin{example}
|
||||
Given the program:
|
||||
\begin{lstlisting}
|
||||
sneezing(X):0.7 ; null:0.3 :- flu(X).
|
||||
sneezing(X):0.8 ; null:0.2 :- hay_fever(X).
|
||||
\end{lstlisting}
|
||||
|
||||
The probability of \texttt{sneezing(bob)} is:
|
||||
\[ \prob{\texttt{sneezing(bob)}} = \prob{w_1} + \prob{w_2} + \prob{w_3} \]
|
||||
\end{example}
|
||||
\end{description}
|
||||
509
src/year1/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
Normal file
509
src/year1/fundamentals-of-ai-and-kr/module2/sections/_prolog.tex
Normal file
@ -0,0 +1,509 @@
|
||||
\chapter{Prolog}
|
||||
|
||||
|
||||
It may be useful to first have a look at the "Logic programming" section of
|
||||
\href{\gitLAAITwo}{\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 in 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 a 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 is undecidable, the 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.
|
||||
\end{itemize}
|
||||
\item Solve the remaining 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}
|
||||
|
||||
|
||||
|
||||
\section{Meta predicates}
|
||||
|
||||
\begin{description}
|
||||
\item[\texttt{call/1}] \marginnote{\texttt{call/1}}
|
||||
Given a term \texttt{T}, \texttt{call(T)} considers \texttt{T} as a predicate and evaluates it.
|
||||
At the time of evaluation, \texttt{T} must be a non-numeric term.
|
||||
|
||||
\begin{example} \phantom{}
|
||||
\begin{lstlisting}
|
||||
p(X) :- call(X).
|
||||
q(a).
|
||||
|
||||
?- p(q(Y)).
|
||||
yes Y=a
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{fail/0}] \marginnote{\texttt{fail/0}}
|
||||
The evaluation of \texttt{fail} always fails, forcing the interpreter to backtrack.
|
||||
|
||||
\begin{example}[Implementation of negation as failure] \phantom{}
|
||||
\begin{lstlisting}[language={}]
|
||||
not(P) :- call(P), !, fail.
|
||||
not(P).
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
\vspace*{-1.5em}
|
||||
Note that the cut followed by \texttt{fail} (\texttt{!, fail}) is useful to force a global failure.
|
||||
|
||||
\item[\texttt{bagof/3} and \texttt{setof/3}] \phantom{}
|
||||
\begin{description}
|
||||
\item[\texttt{bagof/3}] \marginnote{\texttt{bagof/3}}
|
||||
The predicate \texttt{bagof(X, P, L)} unifies \texttt{L} with a list of the instances of \texttt{X} that satisfy \texttt{P}.
|
||||
Fails if none exists.
|
||||
\item[\texttt{sefof/3}] \marginnote{\texttt{sefof/3}}
|
||||
The predicate \texttt{setof(X, P, S)} unifies \texttt{S} with a set of the instances of \texttt{X} that satisfy \texttt{P}.
|
||||
Fails if none exists.
|
||||
|
||||
In practice, for computational reasons, a list (with repetitions) might be computed.
|
||||
\end{description}
|
||||
|
||||
\begin{example} \phantom{}
|
||||
\begin{lstlisting}[language={}]
|
||||
p(1).
|
||||
p(2).
|
||||
p(1).
|
||||
|
||||
?- setof(X, p(X), S).
|
||||
yes S=[1, 2] X=X
|
||||
|
||||
?- bagof(X, p(X), S).
|
||||
yes S=[1, 2, 1] X=X
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
\begin{description}
|
||||
\item[Quantification]
|
||||
When solving a goal, the interpreter unifies free variables with a value.
|
||||
This may cause unwanted behaviors when using \texttt{bagof} or \texttt{setof}.
|
||||
The \texttt{X\textasciicircum} tells the interpreter to not (permanently) bind the variable \texttt{X}.
|
||||
|
||||
\begin{example} \phantom{}\\
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[language={}]
|
||||
father(giovanni, mario).
|
||||
father(giovanni, giuseppe).
|
||||
father(mario, paola).
|
||||
|
||||
?- setof(X, father(X, Y), S).
|
||||
yes X=X Y=giuseppe S=[giovanni];
|
||||
X=X Y=mario S=[giovanni];
|
||||
X=X Y=paola S=[mario]
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[language={}]
|
||||
father(giovanni, mario).
|
||||
father(giovanni, giuseppe).
|
||||
father(mario, paola).
|
||||
|
||||
?- setof(X, Y^father(X, Y), S).
|
||||
yes S=[giovanni, mario] X=X Y=Y
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\end{example}
|
||||
\end{description}
|
||||
|
||||
\item[\texttt{findall/3}] \marginnote{\texttt{findall/3}}
|
||||
The predicate \texttt{findall(X, P, S)} unifies \texttt{S} with a list of the instances of \texttt{X} that satisfy \texttt{P}.
|
||||
If none exists, \texttt{S} is unified with an empty list.
|
||||
Variables in \texttt{P} that do not appear in \texttt{X} are not bound (same as the \texttt{Y\textasciicircum} operator).
|
||||
|
||||
\begin{example} \phantom{}
|
||||
\begin{lstlisting}[language={}]
|
||||
father(giovanni, mario).
|
||||
father(giovanni, giuseppe).
|
||||
father(mario, paola).
|
||||
|
||||
?- findall(X, father(X, Y), S).
|
||||
yes S=[giovanni, mario] X=X Y=Y
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{var/1}] \marginnote{\texttt{var/1}}
|
||||
The predicate \texttt{var(T)} is true if \texttt{T} is a variable.
|
||||
|
||||
\item[\texttt{nonvar/1}] \marginnote{\texttt{nonvar/1}}
|
||||
The predicate \texttt{nonvar(T)} is true if \texttt{T} is not a free variable.
|
||||
|
||||
\item[\texttt{number/1}] \marginnote{\texttt{number/1}}
|
||||
The predicate \texttt{number(T)} is true if \texttt{T} is a number.
|
||||
|
||||
\item[\texttt{ground/1}] \marginnote{\texttt{ground/1}}
|
||||
The predicate \texttt{ground(T)} is true if \texttt{T} does not have free variables.
|
||||
|
||||
\item[\texttt{=../2}] \marginnote{\texttt{=../2}}
|
||||
The operator \texttt{T =.. L} unifies \texttt{L} with a list where
|
||||
its head is the head of \texttt{T} and the tail contains the remaining arguments of \texttt{T}
|
||||
(i.e. puts all the components of a predicate into a list).
|
||||
Only one between \texttt{T} and \texttt{L} can be a variable.
|
||||
|
||||
\begin{example} \phantom{} \\
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[language={}]
|
||||
?- foo(hello, X) =.. List.
|
||||
List = [foo, hello, X]
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[language={}]
|
||||
?- Term =.. [baz, foo(1)].
|
||||
Term = baz(foo(1))
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{clause/2}] \marginnote{\texttt{clause/2}}
|
||||
The predicate \texttt{clause(Head, Body)} is true if it can unify \texttt{Head} and \texttt{Body} with an existing clause.
|
||||
\texttt{Head} must be initialized to a non-numeric term. \texttt{Body} can be a variable or a term.
|
||||
|
||||
\begin{example} \phantom{}
|
||||
\begin{lstlisting}[language={}]
|
||||
p(1).
|
||||
q(X, a) :- p(X), r(a).
|
||||
q(2, Y) :- d(Y).
|
||||
|
||||
?- clause(p(1), B).
|
||||
yes B=true
|
||||
|
||||
?- clause(p(X), true).
|
||||
yes X=1
|
||||
|
||||
?- clause(q(X, Y), B).
|
||||
yes X=_1 Y=a B=p(_1), r(a);
|
||||
X=2 Y=_2 B=d(_2)
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{assert/1}] \marginnote{\texttt{assert/1}}
|
||||
The predicate \texttt{assert(T)} adds \texttt{T} in an unspecified position of the clauses database of Prolog.
|
||||
In other words, it allows to dynamically add clauses.
|
||||
\begin{descriptionlist}
|
||||
\item[\texttt{asserta/1}] \marginnote{\texttt{asserta/1}}
|
||||
As \texttt{assert(T)}, with insertion at the beginning of the database.
|
||||
\item[\texttt{assertz/1}] \marginnote{\texttt{assertz/1}}
|
||||
As \texttt{assert(T)}, with insertion at the end of the database.
|
||||
\end{descriptionlist}
|
||||
|
||||
Note that \texttt{:- assert((p(X)))} quantifies \texttt{X} existentially as it is a query.
|
||||
If it is not ground and added to the database as is,
|
||||
it becomes a clause and therefore quantified universally: $\forall \texttt{X}: \texttt{p(X)}$.
|
||||
|
||||
\begin{example}[Lemma generation] \phantom{}
|
||||
\begin{lstlisting}[language={}]
|
||||
fib(0, 0) :- !.
|
||||
fib(1, 1) :- !.
|
||||
fib(N, F) :- N1 is N-1, fib(N1, F1),
|
||||
N2 is N-2, fib(N2, F2),
|
||||
F is F1+F2,
|
||||
generate_lemma(fib(N, F)).
|
||||
|
||||
generate_lemma(T) :- clause(T, true), !.
|
||||
generate_lemma(T) :- assert(T).
|
||||
\end{lstlisting}
|
||||
|
||||
The custom defined \texttt{generate\_lemma/1} allows to add to the clauses database all the intermediate steps to compute the Fibonacci sequence
|
||||
(similar concept to dynamic programming).
|
||||
\end{example}
|
||||
|
||||
\item[\texttt{retract/1}] \marginnote{\texttt{retract/1}}
|
||||
The predicate \texttt{retract(T)} removes from the database the first clause that unifies with \texttt{T}.
|
||||
|
||||
\item[\texttt{abolish/2}] \marginnote{\texttt{abolish/2}}
|
||||
The predicate \texttt{abolish(T, n)} removes from the database all the occurrences of \texttt{T} with arity \texttt{n}.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Meta-interpreters}
|
||||
|
||||
\begin{description}
|
||||
\item[Meta-interpreter] \marginnote{Meta-interpreter}
|
||||
Interpreter for a language $L_1$ written in another language $L_2$.
|
||||
|
||||
\item[Prolog vanilla meta-interpreter] \marginnote{Vanilla meta-interpreter}
|
||||
The Prolog vanilla meta-interpreter is defined as follows:
|
||||
\begin{lstlisting}[language={}]
|
||||
solve(true) :- !.
|
||||
solve( (A, B) ) :- !, solve(A), solve(B).
|
||||
solve(A) :- clause(A, B), solve(B).
|
||||
\end{lstlisting}
|
||||
|
||||
In other words, the clauses state the following:
|
||||
\begin{enumerate}
|
||||
\item A tautology is a success.
|
||||
\item To prove a conjunction, we have to prove both atoms.
|
||||
\item To prove an atom \texttt{A},
|
||||
we look for a clause \texttt{A :- B} that has \texttt{A} as conclusion and prove its premise \texttt{B}.
|
||||
\end{enumerate}
|
||||
\end{description}
|
||||
@ -0,0 +1,136 @@
|
||||
\chapter{Web reasoning}
|
||||
|
||||
|
||||
\section{Semantic web}
|
||||
|
||||
\begin{description}
|
||||
\item[Semantic web] \marginnote{Semantic web}
|
||||
Method to represent and reason on the data available on the web.
|
||||
Semantic web aims to preserve the characteristics of the web, this includes:
|
||||
\begin{itemize}
|
||||
\item Globality.
|
||||
\item Information distribution.
|
||||
\item Information inconsistency of contents and links (as everyone can publish).
|
||||
\item Information incompleteness of contents and links.
|
||||
\end{itemize}
|
||||
|
||||
Information is structured using ontologies and logic is used as inference mechanism.
|
||||
New knowledge can be derived through proofs.
|
||||
|
||||
\item[Uniform resource identifier] \marginnote{URI}
|
||||
Naming system to uniquely identify concepts.
|
||||
Each URI corresponds to one and only one concept, but multiple URIs can refer to the same concept.
|
||||
|
||||
\item[XML] \marginnote{XML}
|
||||
Markup language to represent hierarchically structured data.
|
||||
An XML can contain in its preamble the description of the grammar used within the document.
|
||||
|
||||
\item[Resource description framework (RDF)] \marginnote{Resource description framework (RDF)}
|
||||
XML-based language to represent knowledge.
|
||||
Based on triplets:
|
||||
\begin{center}
|
||||
\texttt{<subject, predicate, object>}\\
|
||||
\texttt{<resource, attribute, value>}
|
||||
\end{center}
|
||||
|
||||
RDF supports:
|
||||
\begin{descriptionlist}
|
||||
\item[Types] Using the attribute \texttt{type} which can assume an URI as value.
|
||||
\item[Collections] Subjects and objects can be bags, sequences or alternatives.
|
||||
\item[Meta-sentences] Reification of the sentences (e.g. "X says that Y\dots").
|
||||
\end{descriptionlist}
|
||||
|
||||
\begin{description}
|
||||
\item[RDF schema] \marginnote{RDF schema}
|
||||
RDF can be used to describe classes and relations with other classes (e.g. \texttt{type}, \texttt{subClassOf}, \texttt{subPropertyOf}, \dots)
|
||||
|
||||
\item[Representation] \phantom{}
|
||||
\begin{descriptionlist}
|
||||
\item[Graph] A graph where nodes are subjects or objects and edges are predicates.
|
||||
\begin{example} \phantom{}
|
||||
\begin{center}
|
||||
\includegraphics[width=0.4\textwidth]{img/rdf_graph_example.png}
|
||||
\end{center}
|
||||
The graph stands for:
|
||||
\texttt{http://www.example.org/index.html} has a \texttt{creator} with staff id \texttt{85740}.
|
||||
\end{example}
|
||||
|
||||
\item[XML]
|
||||
\begin{example} \phantom{}
|
||||
\begin{lstlisting}[mathescape=true, language=xml]
|
||||
<rdf:RDF
|
||||
xmlns:rdf=http://www.w3.org/1999/02/22-rdf-syntax-ns#
|
||||
xmlns:contact=http://www.w3.org/2000/10/swap/pim/contact#>
|
||||
<contact:Person rdf:about="http://www.w3.org/People/EM/contact#me">
|
||||
<contact:fullName>Eric Miller</contact:fullName>
|
||||
<contact:mailbox rdf:resource="mailto:em@w3.org"/>
|
||||
<contact:personalTitle>Dr.</contact:personalTitle>
|
||||
</contact:Person>
|
||||
</rdf:RDF>
|
||||
\end{lstlisting}
|
||||
\end{example}
|
||||
\end{descriptionlist}
|
||||
|
||||
\item[Database similarities]
|
||||
RDF aims to integrate different databases:
|
||||
\begin{itemize}
|
||||
\item A DB record is an RDF node.
|
||||
\item The name of a column can be seen as a property type.
|
||||
\item The value of a field corresponds to the value of a property.
|
||||
\end{itemize}
|
||||
\end{description}
|
||||
|
||||
\item[RDFa] \marginnote{RDFa}
|
||||
Specification to integrate XHTML and RDF.
|
||||
|
||||
\item[SPARQL] \marginnote{SPARQL}
|
||||
Language to query different data sources that support RDF (natively or through a middleware).
|
||||
|
||||
\item[Ontology web language (OWL)] \marginnote{Ontology web language (OWL)}
|
||||
Ontology-based on RDF and description logic fragments.
|
||||
Three levels of expressivity are available:
|
||||
\begin{itemize}
|
||||
\item OWL lite.
|
||||
\item OWL DL.
|
||||
\item OWL full.
|
||||
\end{itemize}
|
||||
|
||||
An OWL has:
|
||||
\begin{descriptionlist}
|
||||
\item[Classes] Categories.
|
||||
\item[Properties] Roles and relations.
|
||||
\item[Instances] Individuals.
|
||||
\end{descriptionlist}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Knowledge graphs}
|
||||
|
||||
\begin{description}
|
||||
\item[Knowledge graph] \marginnote{Knowledge graph}
|
||||
Knowledge graphs overcome the computational complexity of T-box reasoning with semantic web and description logics.
|
||||
|
||||
\begin{itemize}
|
||||
\item Use a simple vocabulary with a simple but robust corpus of types and properties adopted as a standard.
|
||||
\item Represent a graph with terms as nodes and edges connecting them.
|
||||
Knowledge is therefore represented as triplets \texttt{(h, r, t)} where \texttt{h} and \texttt{t} are entities and \texttt{r} is a relation.
|
||||
\item Logic formulas are removed. T-box and A-box can be seen as the same concept. There is no reasoning but only facts.
|
||||
\item Data does not have a conceptual schema and can come from different sources with different semantics.
|
||||
\item Graph algorithms to traverse the graph and solve queries.
|
||||
\end{itemize}
|
||||
|
||||
\item[KG quality] \marginnote{Quality}
|
||||
\begin{description}
|
||||
\item[Coverage] If the graph has all the required information.
|
||||
\item[Correctness] If the information is correct (can be objective or subjective).
|
||||
\item[Freshness] If the content is up-to-date.
|
||||
\end{description}
|
||||
|
||||
\item[Graph embedding] \marginnote{Graph embedding}
|
||||
Project entities and relations into a vectorial space for ML applications.
|
||||
\begin{description}
|
||||
\item[Link prediction] Given two entities \texttt{h} and \texttt{t}, determine the relation \texttt{r} between them.
|
||||
\item[Entity prediction] Given an entity \texttt{h} and a relation \texttt{t}, determine an entity \texttt{t}-related to \texttt{h}.
|
||||
\end{description}
|
||||
\end{description}
|
||||
@ -0,0 +1,374 @@
|
||||
\chapter{Time reasoning}
|
||||
|
||||
|
||||
\section{Propositional logic}
|
||||
|
||||
\begin{description}
|
||||
\item[State] \marginnote{State}
|
||||
The current state of the world can be represented as a set of propositions that are true according to the observation of an agent.
|
||||
|
||||
The union of a countable sequence of states represents the evolution of the world. Each proposition is distinguished by its time step.
|
||||
|
||||
\begin{example}
|
||||
A child has a bow and an arrow and then shoots the arrow.
|
||||
\[
|
||||
\begin{split}
|
||||
\text{KB}^0 &= \{ \texttt{hasBow}^0, \texttt{hasArrow}^0 \} \\
|
||||
\text{KB}^1 &= \{ \texttt{hasBow}^0, \texttt{hasArrow}^0, \texttt{hasBow}^1, \lnot\texttt{hasArrow}^1 \}
|
||||
\end{split}
|
||||
\]
|
||||
\end{example}
|
||||
|
||||
\item[Action] \marginnote{Action}
|
||||
An action indicates how a state evolves into the next one.
|
||||
It is described using effect axioms in the form:
|
||||
\[ \texttt{action}^t \Rightarrow (\texttt{preconditions}^t \iff \texttt{effects}^{t+1}) \]
|
||||
|
||||
\begin{description}
|
||||
\item[Frame problem] \marginnote{Frame problem}
|
||||
The effect axioms of an action do not tell what remains unchanged in the next state.
|
||||
|
||||
\begin{description}
|
||||
\item[Frame axioms] \marginnote{Frame axioms}
|
||||
The frame axioms of an action describe the unaffected propositions of an action.
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
\begin{example}
|
||||
The action of shooting an arrow can be described as:
|
||||
\[
|
||||
\begin{split}
|
||||
\texttt{SHOOT}^t &\Rightarrow \{ \texttt{hasArrow}^t \iff \lnot\texttt{hasArrow}^{t+1} \} \\
|
||||
\texttt{SHOOT}^t &\Rightarrow \{ \texttt{hasBow}^t \iff \texttt{hasBow}^{t+1} \}
|
||||
\end{split}
|
||||
\]
|
||||
\end{example}
|
||||
|
||||
Note that with $m$ actions and $n$ propositions, the number of frame axioms will be of order $O(mn)$.
|
||||
Inference for $t$ time steps will have complexity $O(nt)$.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Situation calculus (Green's formulation)}
|
||||
Situation calculus uses first-order logic instead of propositional logic.
|
||||
|
||||
\begin{description}
|
||||
\item[Situation] \marginnote{Situation}
|
||||
The initial state is a situation.
|
||||
Applying an action in a situation is a situation:
|
||||
\[ s \text{ is a situation and } \texttt{a} \text{ is an action} \iff \texttt{result}(\texttt{a}, s) \text{ is situation} \]
|
||||
(Note: in FAIRK module 1, \texttt{result} is denoted as \texttt{do}).
|
||||
|
||||
\item[Fluent] \marginnote{Fluent}
|
||||
Function that varies depending on the situation
|
||||
(i.e. tells if a property holds in a given situation).
|
||||
|
||||
\begin{example}
|
||||
$\texttt{hasBow}(s)$ where $s$ is a situation.
|
||||
\end{example}
|
||||
|
||||
\item[Action] \marginnote{Action}
|
||||
Actions are described using:
|
||||
\begin{descriptionlist}
|
||||
\item[Possibility axioms] \marginnote{Possibility axioms}
|
||||
Indicates the preconditions $\phi_\texttt{a}$ of an action \texttt{a} in a given situation $s$:
|
||||
\[ \phi_\texttt{a}(s) \Rightarrow \texttt{poss}(\texttt{a}, s) \]
|
||||
|
||||
\item[Successor state axiom] \marginnote{Successor state axiom}
|
||||
The evolution of a fluent $F$ follows the axiom:
|
||||
\[ F^{t+1} \iff (\texttt{ActionCauses$(F)$} \vee (F^{t} \land \lnot\texttt{ActionCauses$(\lnot F)$})) \]
|
||||
In other words, a fluent is true if an action makes it true or does not change if the action does not involve it.
|
||||
|
||||
Adding the notion of possibility, an action can be described as:
|
||||
\[
|
||||
\begin{split}
|
||||
\texttt{poss}&(\texttt{a}, s) \Rightarrow \Big( F(\texttt{result}(\texttt{a}, s)) \iff \\
|
||||
& (\texttt{a} = \texttt{ActionCauses$(F)$}) \,\vee\, \\
|
||||
& (F(s) \,\land\, \texttt{a} \neq \lnot\texttt{ActionCauses$(\lnot F)$})
|
||||
\Big)
|
||||
\end{split}
|
||||
\]
|
||||
|
||||
\item[Unique action axiom] \marginnote{Unique action axiom}
|
||||
Only a single action can be executed in a situation to avoid non-determinism.
|
||||
\end{descriptionlist}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Event calculus (Kowalski's formulation)}
|
||||
|
||||
Event calculus reifies fluents and events (actions) as terms (instead of predicates).
|
||||
|
||||
\begin{description}
|
||||
\item[Event calculus ontology] \marginnote{Event calculus ontology}
|
||||
A fixed set of predicates:
|
||||
\begin{descriptionlist}
|
||||
\item[$\texttt{holdsAt}(F, T)$] The fluent $F$ holds at time $T$.
|
||||
\item[$\texttt{happens}(\texttt{E}, T)$] The event \texttt{E} (i.e. execution of an action) happened at time $T$.
|
||||
\item[$\texttt{initiates}(\texttt{E}, F, T)$] The event \texttt{E} causes the fluent $F$ to start holding at time $T$.
|
||||
\item[$\texttt{terminates}(\texttt{E}, F, T)$] The event \texttt{E} causes the fluent $F$ to cease holding at time $T$.
|
||||
\item[$\texttt{clipped}(T_i, F, T_j)$] The fluent $F$ has been made false between the times $T_i$ and $T_j$ ($T_i < T_j$).
|
||||
\item[$\texttt{initially}(F)$] The fluent $F$ holds at time 0.
|
||||
\end{descriptionlist}
|
||||
|
||||
\item[Domain-independent axioms] \marginnote{Domain-independent axioms}
|
||||
A fixed set of axioms:
|
||||
\begin{description}
|
||||
\item[Truthness of a fluent] \phantom{}
|
||||
\begin{enumerate}
|
||||
\item A fluent holds if an event initiated it in the past and has not been clipped.
|
||||
\[
|
||||
\begin{split}
|
||||
\texttt{holdsAt}(F, T_j) \Leftarrow\, &\texttt{happens}(\texttt{E}, T_i) \land (T_i < T_j) \,\land\\
|
||||
&\texttt{initiates}(\texttt{E}, F, T_i) \land \lnot\texttt{clipped}(T_i, F, T_j)
|
||||
\end{split}
|
||||
\]
|
||||
|
||||
\item A fluent holds if it was initially true and has not been clipped.
|
||||
\[ \texttt{holdsAt}(F, T) \Leftarrow\, \texttt{initially}(F) \land \lnot\texttt{clipped}(0, F, T) \]
|
||||
\end{enumerate}
|
||||
Note: the negations make the definition of these axioms in Prolog unsafe.
|
||||
|
||||
\item[Clipping of a fluent]
|
||||
\[ \texttt{clipped}(T_i, F, T_j) \Leftarrow \texttt{happens}(\texttt{E}, T) \land (T_i < T < T_j) \land \texttt{terminates}(\texttt{E}, F, T) \]
|
||||
\end{description}
|
||||
|
||||
\item[Domain-dependent axioms] \marginnote{Domain-dependent axioms}
|
||||
Domain-specific axioms defined using the predicates\\\texttt{initially}, \texttt{initiates} and \texttt{terminates}.
|
||||
\end{description}
|
||||
|
||||
\begin{description}
|
||||
\item[Deductive reasoning]
|
||||
Event calculus only allows deductive reasoning:
|
||||
it takes as input the domain-dependant axioms and a set of events and computes a set of true fluents.
|
||||
If a new event is observed, the query needs to be recomputed again.
|
||||
\end{description}
|
||||
|
||||
|
||||
\begin{example}
|
||||
A room with a light and a button can be described as:
|
||||
\begin{descriptionlist}
|
||||
\item[Fluents] \texttt{lightOn} $\cdot$ \texttt{lightOff}
|
||||
\item[Events] \texttt{PUSH\_BUTTON}
|
||||
\end{descriptionlist}
|
||||
|
||||
Domain-dependent axioms are:
|
||||
\begin{descriptionlist}
|
||||
\item[Initial state] \texttt{initially}(\texttt{lightOff})
|
||||
\item[Effects of \texttt{PUSH\_BUTTON} on \texttt{lightOn}] \phantom{}
|
||||
\begin{itemize}
|
||||
\item $\texttt{initiates}(\texttt{PUSH\_BUTTON}, \texttt{lightOn}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOff}, T)$
|
||||
\item $\texttt{terminates}(\texttt{PUSH\_BUTTON}, \texttt{lightOn}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOn}, T)$
|
||||
\end{itemize}
|
||||
\item[Effects of \texttt{PUSH\_BUTTON} on \texttt{lightOff}] \phantom{}
|
||||
\begin{itemize}
|
||||
\item $\texttt{initiates}(\texttt{PUSH\_BUTTON}, \texttt{lightOff}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOn}, T)$
|
||||
\item $\texttt{terminates}(\texttt{PUSH\_BUTTON}, \texttt{lightOff}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOff}, T)$
|
||||
\end{itemize}
|
||||
\end{descriptionlist}
|
||||
|
||||
A set of events could be:
|
||||
\[ \texttt{happens}(\texttt{PUSH\_BUTTON}, 3) \cdot \texttt{happens}(\texttt{PUSH\_BUTTON}, 5) \cdot \texttt{happens}(\texttt{PUSH\_BUTTON}, 6) \]
|
||||
\end{example}
|
||||
|
||||
|
||||
\subsection{Reactive event calculus}
|
||||
\marginnote{Reactive event calculus}
|
||||
|
||||
Allows to add events dynamically without the need to recompute the result.
|
||||
|
||||
|
||||
|
||||
\section{Allen's logic of intervals}
|
||||
|
||||
Event calculus only captures instantaneous events that happen at given points in time.
|
||||
|
||||
\begin{description}
|
||||
\item[Allen's logic of intervals] \marginnote{Allen's logic of intervals}
|
||||
Reasoning on time intervals.
|
||||
|
||||
\begin{description}
|
||||
\item[Interval] \marginnote{Interval}
|
||||
An interval $i$ starts at a time $\texttt{begin}(i)$ and ends at a time $\texttt{end}(i)$.
|
||||
|
||||
\item[Temporal operators] \marginnote{Temporal operators}
|
||||
\begin{itemize}
|
||||
\item $\texttt{meet}(i, j) \iff \texttt{end}(i) = \texttt{begin}(j)$
|
||||
\item $\texttt{before}(i, j) \iff \texttt{end}(i) < \texttt{begin}(j)$
|
||||
\item $\texttt{after}(i, j) \iff \texttt{before}(j, i)$
|
||||
\item $\texttt{during}(i, j) \iff \texttt{begin}(j) < \texttt{begin}(i) < \texttt{end}(i) < \texttt{end}(j)$
|
||||
\item $\texttt{overlap}(i, j) \iff \texttt{begin}(i) < \texttt{begin}(j) < \texttt{end}(i) < \texttt{end}(j)$
|
||||
\item $\texttt{starts}(i, j) \iff \texttt{begin}(i) = \texttt{begin}(j)$
|
||||
\item $\texttt{finishes}(i, j) \iff \texttt{end}(i) = \texttt{end}(j)$
|
||||
\item $\texttt{equals}(i, j) \iff \texttt{starts}(i, j) \land \texttt{ends}(i, j)$
|
||||
\end{itemize}
|
||||
|
||||
\begin{figure}[H]
|
||||
\centering
|
||||
\includegraphics[width=0.5\textwidth]{img/allen_intervals.png}
|
||||
\caption{Visual representation of temporal operators}
|
||||
\end{figure}
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Modal logics}
|
||||
|
||||
Logic-based on interacting agents with their own knowledge base.
|
||||
|
||||
\begin{description}
|
||||
\item[Propositional attitudes] \marginnote{Propositional attitudes}
|
||||
Operators to represent knowledge and beliefs of an agent towards the environment and other agents.
|
||||
|
||||
First-order logic is not suited to represent these operators.
|
||||
|
||||
\item[Modal logics] \marginnote{Modal logics}
|
||||
Modal logics have the same syntax as first-order logic with the addition of modal operators.
|
||||
|
||||
\item[Modal operator]
|
||||
A modal operator takes as input the name of an agent and a sentence (instead of a term as in FOL).
|
||||
|
||||
\begin{description}
|
||||
\item[Knowledge operator] \marginnote{Knowledge operator}
|
||||
Operator to indicate that an agent \texttt{a} knows $P$:
|
||||
\[ \textbf{K}_\texttt{a}(P) \]
|
||||
|
||||
\item[Belief operator]
|
||||
\item[Everyone knows operator]
|
||||
\item[Common knowledge operator]
|
||||
\item[Distribute knowledge operator]
|
||||
\end{description}
|
||||
|
||||
Depending on the operators, different modal logics can be defined.
|
||||
|
||||
\item[Semantics]
|
||||
An agent has a current perception of the world and considers the unknown as other possible worlds.
|
||||
Moreover, if $P$ is true in any accessible world from the current one, the agent has knowledge of $P$.
|
||||
|
||||
Formally, semantics is defined on a set of primitive propositions $\phi$
|
||||
using a Kripke structure $M = (S, \pi, K_\texttt{1}, \dots, K_\texttt{n})$ where:
|
||||
\begin{itemize}
|
||||
\item $S$ is a set of the states of the world.
|
||||
\item $\pi: \phi \rightarrow 2^S$ specifies in which states each primitive proposition holds.
|
||||
\item $K_\texttt{i} \subseteq S \times S$ is a binary relation where
|
||||
$(s, t) \in K_\texttt{i}$ if an agent \texttt{i} considers the world $t$ possible (accessible) from $s$.
|
||||
In other words, when the agent is in the world $s$, it considers $t$ to also be a possibly valid world.
|
||||
Obviously, $(s, s) \in K_\texttt{i}$ for all states.
|
||||
\end{itemize}
|
||||
|
||||
\begin{example}
|
||||
Alice is in a room and tosses a coin. Bob is in another room and will enter Alice's room when the coin lands to observe the result.
|
||||
|
||||
We define a model $M = (S, \pi, K_\texttt{a}, K_\texttt{b})$ on $\phi$ where:
|
||||
\begin{itemize}
|
||||
\item $\phi = \{ \texttt{tossed}, \texttt{heads}, \texttt{tails} \}$.
|
||||
\item $S = \{ s_0, h_1, t_1, h_2, t_2 \}$ where the possible states are divided in three stages:
|
||||
the initial state ($s_0$), the result of the coin flip ($h_1, t_1$) and the observation of Bob ($h_2, t_2$).
|
||||
\item
|
||||
$\pi(\texttt{tossed}) = \{ h_1, t_1, h_2, t_2 \}$\\
|
||||
$\pi(\texttt{heads}) = \{ h_1, h_2 \}$\\
|
||||
$\pi(\texttt{tails}) = \{ t_1, t_2 \}$
|
||||
\item
|
||||
$K_\texttt{a} = \{ (s, s) \mid s \in S \}$ as Alice observes everything in each world and does not have uncertainty.\\
|
||||
$K_\texttt{b} = \{ (s, s) \mid s \in S \} \cup \{ (h_1, t_1), (t_1, h_1) \}$ as Bob is unsure of what happens in the second stage.\\
|
||||
\end{itemize}
|
||||
\vspace*{-1em}
|
||||
With this model, we can determine the truthness of sentences like:
|
||||
\[ (M, s_0) \models K_\texttt{a}(\lnot\texttt{tossed}) \land K_\texttt{b}\Big(K_\texttt{a}\big(K_\texttt{b}(\lnot \texttt{heads} \land \lnot \texttt{tails})\big)\Big) \]
|
||||
\[ (M, t_1) \models (\texttt{heads} \vee \texttt{tails}) \land \lnot\texttt{K}_\texttt{b}(\texttt{heads}) \land
|
||||
\lnot\texttt{K}_\texttt{b}(\texttt{tails}) \land
|
||||
\texttt{K}_\texttt{b}(\texttt{K}_\texttt{a}(\texttt{heads}) \vee \texttt{K}_\texttt{a}(\texttt{tails})) \]
|
||||
\end{example}
|
||||
|
||||
\item[Axioms] \phantom{}
|
||||
\begin{description}
|
||||
\item[Tautology]
|
||||
All propositional tautologies are valid.
|
||||
|
||||
\item[Modus ponens]
|
||||
If $\varphi$ and $\varphi \Rightarrow \psi$ are valid, then $\psi$ is valid.
|
||||
|
||||
\item[Distribution axiom]
|
||||
Knowledge is closed under implication:
|
||||
\[ (K_\texttt{i}(\varphi) \land K_\texttt{i}(\varphi \Rightarrow \psi)) \Rightarrow K_\texttt{i}(\psi) \]
|
||||
|
||||
\item[Knowledge generalization rule]
|
||||
An agent knows all the tautologies:
|
||||
\[ \forall \text{ structures } M: (M \models \varphi) \Rightarrow (M \models K_\texttt{i}(\varphi)) \]
|
||||
|
||||
\item[Knowledge axiom]
|
||||
If an agent knows $\varphi$, then $\varphi$ is true:
|
||||
\[ K_\texttt{i}(\varphi) \Rightarrow \varphi \]
|
||||
|
||||
In belief logic, this axiom is substituted with $\lnot K_\texttt{i}(\texttt{false})$.
|
||||
|
||||
\item[Introspection axioms]
|
||||
An agent is sure of its knowledge:
|
||||
\begin{description}
|
||||
\item[Positive] $K_\texttt{i}(\varphi) \Rightarrow K_\texttt{i}(K_\texttt{i}(\varphi))$
|
||||
\item[Negative] $\lnot K_\texttt{i}(\varphi) \Rightarrow K_\texttt{i}(\lnot K_\texttt{i}(\varphi))$
|
||||
\end{description}
|
||||
\end{description}
|
||||
|
||||
Different modal logics can be defined based on the validity of these axioms.
|
||||
\end{description}
|
||||
|
||||
|
||||
|
||||
\section{Temporal logics}
|
||||
|
||||
Logics based on modal logic with the addition of a temporal dimension.
|
||||
Time is discrete and each world is labeled with an integer.
|
||||
The accessibility relation maps into the temporal dimension with two possible evolution alternatives:
|
||||
\begin{descriptionlist}
|
||||
\item[Linear-time] \marginnote{Linear-time}
|
||||
From each world, there is only one other accessible world.
|
||||
|
||||
\item[Branching-time] \marginnote{Branching-time}
|
||||
From each world, there are many accessible worlds.
|
||||
\end{descriptionlist}
|
||||
|
||||
|
||||
|
||||
|
||||
\subsection{Linear-time temporal logic}
|
||||
|
||||
\begin{description}
|
||||
\item[Operators] \phantom{}
|
||||
\begin{description}
|
||||
\item[Next ($\bigcirc \varphi$)] \marginnote{Next}
|
||||
$\varphi$ is true in the next time step.
|
||||
|
||||
\item[Globally ($\square \varphi$)] \marginnote{Globally}
|
||||
$\varphi$ is always true from now on.
|
||||
|
||||
\item[Future ($\diamond \varphi$)] \marginnote{Future}
|
||||
$\varphi$ is sometimes true in the future.
|
||||
It is equivalent to $\lnot\square(\lnot \varphi)$.
|
||||
|
||||
\item[Until ($\varphi \mathcal{U} \psi$)] \marginnote{Until}
|
||||
There exists a moment (now or in the future) when $\psi$ holds.
|
||||
$\varphi$ is guaranteed to hold from now until $\psi$ starts to hold.
|
||||
|
||||
\item[Weak until ($\varphi \mathcal{W} \psi$)] \marginnote{Weak until}
|
||||
There might be a moment when $\psi$ holds.
|
||||
$\varphi$ is guaranteed to hold from now until $\psi$ possibly starts to hold.
|
||||
\end{description}
|
||||
|
||||
\item[Semantics]
|
||||
Given a Kripke structure, $M = (S, \pi, K_\texttt{1}, \dots, K_\texttt{n})$ where states are represented using integers,
|
||||
the semantics of the operators is the following:
|
||||
\begin{itemize}
|
||||
\item $(M, i) \models P \iff i \in \pi(P)$.
|
||||
\item $(M, i) \models \bigcirc\varphi \iff (M, i+1) \models \varphi$.
|
||||
\item $(M, i) \models \square\varphi \iff \forall j \geq i: (M, j) \models \varphi$.
|
||||
\item $(M, i) \models \varphi \mathcal{U} \psi \iff \exists k \geq i: \big( (M, k) \models \psi \,\land\, \forall j. i \leq j \leq k: (M, j) \models \varphi \big)$.
|
||||
\item $(M, i) \models \varphi \mathcal{W} \psi \iff ((M, i) \models \varphi \mathcal{U} \psi) \vee ((M, i) \models \square\varphi)$.
|
||||
\end{itemize}
|
||||
|
||||
\item[Model checking] \marginnote{Model checking}
|
||||
Methods to prove properties of linear-time temporal logic-based finite state machines or distributed systems.
|
||||
\end{description}
|
||||
Reference in New Issue
Block a user