diff --git a/docs/source/tutorials/forall_tutorial.rst b/docs/source/tutorials/forall_tutorial.rst new file mode 100644 index 00000000..2eadff31 --- /dev/null +++ b/docs/source/tutorials/forall_tutorial.rst @@ -0,0 +1,163 @@ +.. _forall_tutorial: + +PyReason Forall Functionality +================================= + +In this tutorial, we will look at how to utilize the forall function in a knowledge graph. The rule will fire only when all of the groundings of a given clause are true. +A grounding is what will substitute a value for a variable in a logic statement. +In the example outlined in the tutorial, the groundings of x are the people who have access to the message. +For Viewed(x), x is the variable, for Viewed(Zach), Zach is the value, and Viewed(Zach) is a grounding. + + +.. note:: + Find the full, executable code `here `_ + +The following graph represents a network of People and a Text Message in their group chat. This graph is directed, meaning the relationship is not reciprocated. + +.. image:: ../../../media/group_chat_graph.png + :align: center + + +Graph +------------ + +First, we create the graph using Networkx. This graph has nodes ``Zach``, ``Justin``, ``Michelle``, ``Amy``, and ``TextMessages``. +The graph we create is directed to show a one-sided relationship. + +.. code:: python + + import networkx as nx + + # Create an empty graph + # Use a directed graph: undirected edges are loaded as two directed edges, + # which doubles the groundings that percent thresholds count. + G = nx.DiGraph() + + # Add nodes + G.add_nodes_from(["TextMessage", "Zach", "Justin", "Michelle", "Amy"]) + + # Add edges + G.add_edges_from([ + ("Zach", "TextMessage", {"HaveAccess": 1}), + ("Justin", "TextMessage", {"HaveAccess": 1}), + ("Michelle", "TextMessage", {"HaveAccess": 1}), + ("Amy", "TextMessage", {"HaveAccess": 1}), + ]) + +Then initialize and load the graph into PyReason with: + +.. code:: python + + import pyreason as pr + # Clears out the state from any previous runs + pr.reset() + pr.reset_rules() + # PyReason will not print information on the screen while this runs, will utilize print statement later on. + pr.settings.verbose = False + pr.load_graph(G) + + +Rules +----- + +Considering that we only want a text message to be considered viewed by all if it has been viewed by everyone that can view it, we define the rule as follows: + +.. code-block:: python + + pr.add_rule(pr.Rule( + "ViewedByAll(y) <- HaveAccess(x,y), forall(Viewed(x))", + "viewed_by_all_rule", + )) + +The ``head`` of the rule is ``ViewedByAll(y)`` and the body is ``HaveAccess(x,y), forall(Viewed(x))``. + +The arrow ``<-`` means the head is inferred in the same timestep the body holds. +Therefore ``<-1`` would infer the head one timestamp after the body is true. + + + +``Viewed(x)`` checks to see if each grounding of ``x`` is true (or in this case has viewed the message). By wrapping the clause in ``forall(...)`` it fires only once all the groundings are true (in this case viewed the message). + +Without ``forall()``, ``Viewed(x)`` would fire at t=0 because Zach and Justin have seen the message at timestep ``0``. +Since ``forall()`` only fires when all users have seen the message at timestep ``2``. + +Facts +----- + +The facts determine the initial conditions of elements in the graph. They can be specified from the graph attributes but in that +case they will be immutable later on. Adding PyReason facts gives us more flexibility. + +In our case we want one person to view the ``TextMessage`` at a particular timestep. +For example, we create facts stating: + + - ``Zach`` and ``Justin`` view the ``TextMessage`` at timestep ``0`` + - ``Michelle`` views the ``TextMessage`` at timestep ``1`` + - ``Amy`` views the ``TextMessage`` at timestep ``2`` + - Viewed fact holds true until timestep ``3`` . + +This allows us to see at what timestamp the ``forall(..)`` rule fires. + +.. code:: python + + pr.add_fact(pr.Fact("Viewed(Zach)", "seen-fact-zach", 0, 3)) + pr.add_fact(pr.Fact("Viewed(Justin)", "seen-fact-justin", 0, 3)) + pr.add_fact(pr.Fact("Viewed(Michelle)", "seen-fact-michelle", 1, 3)) + pr.add_fact(pr.Fact("Viewed(Amy)", "seen-fact-amy", 2, 3)) + + +Running PyReason +---------------- + +To run the reasoning in the file: + +.. code:: python + + # Run the program until timestep 3 to see the forall(..) function fire + interpretation = pr.reason(timesteps=3) + + # filter and sort nodes based on specific attributes + dataframes = pr.filter_and_sort_nodes(interpretation, ["ViewedByAll"]) + # Display filtered node and edge data + for t, df in enumerate(dataframes): + print(f"TIMESTEP - {t}") + print(df) + print() + +This specifies how many timesteps to run for and will format the output to display the filtered node and edge data. +Each pass through this loop will iterate through one timestep and display the data frame entries at each one. + + +Expected output +--------------- +After running the python file, the expected output is: + +.. code:: text + + Added 0 graph-attribute node facts and 4 graph_attribute edge facts. + + TIMESTEP - 0 + Empty DataFrame + Columns: [component, ViewedByAll] + Index: [] + + TIMESTEP - 1 + Empty DataFrame + Columns: [component, ViewedByAll] + Index: [] + + TIMESTEP - 2 + component ViewedByAll + 0 TextMessage [1.0, 1.0] + + TIMESTEP - 3 + component ViewedByAll + 0 TextMessage [1.0, 1.0] + + +1. For timestep 0, we set ``Zach -> Viewed: [1,1]`` and ``Justin -> Viewed: [1,1]`` in the facts +2. For timestep 1, ``Michelle`` views the TextMessage as stated in facts ``Michelle -> Viewed: [1,1]``. +3. For timestep 2, since ``Amy`` has just viewed the ``TextMessage``, therefore ``Amy -> Viewed: [1,1]``. As per the rule, + since all the people have viewed the ``TextMessage``, the message is marked as ``ViewedByAll``. Timestep 2 is the first + timestep where every grounding holds, hence why ``forall()`` fires there. +4. For timestep 3, ``forall()`` still holds true because the message is still ``ViewedByAll`` since ``Viewed`` facts hold + through timestep 3. diff --git a/docs/source/tutorials/index.rst b/docs/source/tutorials/index.rst index 9b14d791..182fd18c 100644 --- a/docs/source/tutorials/index.rst +++ b/docs/source/tutorials/index.rst @@ -23,4 +23,5 @@ Contents ./load_rules_facts_from_file.rst ./llm_generated_rules.rst ./natural_language_to_pyreason.rst + ./forall_tutorial.rst diff --git a/examples/forall_threshold_ex.py b/examples/forall_threshold_ex.py new file mode 100644 index 00000000..378d4a11 --- /dev/null +++ b/examples/forall_threshold_ex.py @@ -0,0 +1,53 @@ +# Example: the forall() quantifier in rule bodies. +# +# forall(clause) is shorthand for a custom threshold of +# Threshold("greater_equal", ("percent", "total"), 100) on that clause: +# the rule only fires when ALL groundings of the clause are satisfied. +# +# This is the group-chat example from the custom thresholds tutorial, +# rewritten without any explicit Threshold objects. A text message is +# ViewedByAll only once every person with access to it has viewed it. +import networkx as nx +import pyreason as pr + +# Use a directed graph: undirected edges are loaded as two directed edges, +# which doubles the groundings that percent thresholds count. +G = nx.DiGraph() +G.add_nodes_from(["TextMessage", "Zach", "Justin", "Michelle", "Amy"]) +G.add_edges_from([ + ("Zach", "TextMessage", {"HaveAccess": 1}), + ("Justin", "TextMessage", {"HaveAccess": 1}), + ("Michelle", "TextMessage", {"HaveAccess": 1}), + ("Amy", "TextMessage", {"HaveAccess": 1}), +]) + +pr.reset() +pr.reset_rules() +pr.settings.verbose = False +pr.load_graph(G) +# Equivalent to passing: +# custom_thresholds=[ +# pr.Threshold("greater_equal", ("number", "total"), 1), +# pr.Threshold("greater_equal", ("percent", "total"), 100), +# ] +# with the rule text "ViewedByAll(y) <- HaveAccess(x,y), Viewed(x)" +pr.add_rule(pr.Rule( + "ViewedByAll(y) <- HaveAccess(x,y), forall(Viewed(x))", + "viewed_by_all_rule", +)) + +# Zach and Justin view the message at t=0, Michelle at t=1, Amy at t=2 +pr.add_fact(pr.Fact("Viewed(Zach)", "seen-fact-zach", 0, 3)) +pr.add_fact(pr.Fact("Viewed(Justin)", "seen-fact-justin", 0, 3)) +pr.add_fact(pr.Fact("Viewed(Michelle)", "seen-fact-michelle", 1, 3)) +pr.add_fact(pr.Fact("Viewed(Amy)", "seen-fact-amy", 2, 3)) + +interpretation = pr.reason(timesteps=3) + +# ViewedByAll(TextMessage) should first appear at t=2, when the last +# person (Amy) views the message. +dataframes = pr.filter_and_sort_nodes(interpretation, ["ViewedByAll"]) +for t, df in enumerate(dataframes): + print(f"TIMESTEP - {t}") + print(df) + print()