chore: improve readme

README.md

@@ -1,58 +1,7 @@
-## Knowledge Representation
-with Horn Clauses
+# On the role of computational logic in MAS: practice with 2P-Kt 4 hours
 
-### Goals
+4h lecture at EASS 2023, held by [Giovanni Ciatto](mailto:giovanni.ciatto@unibo.it)
 
-- Understand basic notions such as:
-    * terms
-    * clauses (facts, rules, goals)
-    * propositional vs. relational representations
-    * logic variables
-    * extensional vs. intensional representations
-    * unifiers and substitutions
-    * unification and MGU
+## Abstract
 
-### Overview
-
-- Horn clauses
-    * Motivations
-        + nice expressiveness-tractability trade-off
-        + basis for Prolog and LP
-        + very well established: tons of literature, theorems, technologies
-    * Overall syntax (notice the difference among terms and clauses)
-    * 2P-Kt as the underlying technology for examples
-- Representing objects with terms
-    * Syntax for terms (skip variables)
-    * Examples:
-        - How to consturct Peano integers
-        - How to construct data structures with terms (e.g. lists)
-- Representing propositions, sets, or relations with predicates
-    * Syntax for horn clauses
-    * Examples
-    * Defining propositions, sets, or relations via clauses
-        + Sets as unary predicates, Relations as N-ary predicates, Propositions as 0-ary predicates
-        + How to construct sets (e.g. nat/1, lst/1)
-        + How to construct relations (e.g. succ/2, member/2, sum/3, append/3)
-- Prolog trick:
-    * same syntax for both terms and predicates 
-        + making them interchaengable
-- Propositional vs. Relational representations?
-- Logic variables: 
-    * Recall overall syntax, highlighting variables
-    * Purpose: placeholders for unknown terms (representing unknown entities)
-    * Definitions: ground term/clause/theory
-    * Extensional vs. Intensional: 
-        + logic variables support intensional representations via non-ground clauses
-        * otherwise one would require all information to be extensionally represented via ground clauses
-    * Two powerful mechanisms:
-        * Unification: computes a substitution making two terms/clauses equal
-        * Resolution: attempts to prove a goal true or not
-        * Both rely on the notion of subtitution
-- Unifier: a mapping among variables and terms (possibly attained via unification)
-    * Can be empty
-    * Can be _applied_ to a term, producing a new term
-    * Substituion: the result of unification or resolution
-        - Can be failed, or a unifier
-- Unification: algorithms to compute the most general unifier (MGU) among 2 terms 
-    * Unification table
-    * Mention the Martelli and Montanari algorithm
+Computational logic (CL) is a key enabler of intelligent behaviour for software agents. Theoretically, it supports key cognitive capabilities such as intensional knowledge representation, automated reasoning, deliberation, etc. When it comes to practice, logic-based technologies are often built on top, or as extensions of, the Prolog language—and the definite clauses (a.k.a. Horn clauses) logic (DCL) behind it. Stemming from a summary of the fundamental notions behind DCL, and logic unification and resolution, this tutorial discusses the impact of CL on the engineering of intelligent agents. Practical demonstrations and examples are provided by means of the 2P-Kt technology, which is a logic-based ecosystem where individual CL mechanisms can be exploited, combined, and possibly extended or modified to support agents’ cognitive capabilities—including, not limited to, automated reasoning.