From 1ee01546f01f7855ce2a9b9f764c77c46403d4b0 Mon Sep 17 00:00:00 2001 From: Julianna Bucci Date: Fri, 25 Sep 2026 11:11:47 -0400 Subject: [PATCH 1/4] Add forall() tutorial and example and index --- docs/source/tutorials/forall_tutorial.rst | 151 ++++++++++++++++++++++ docs/source/tutorials/index.rst | 1 + examples/forall_threshold_ex.py | 76 +++++++++++ 3 files changed, 228 insertions(+) create mode 100644 docs/source/tutorials/forall_tutorial.rst create mode 100644 examples/forall_threshold_ex.py diff --git a/docs/source/tutorials/forall_tutorial.rst b/docs/source/tutorials/forall_tutorial.rst new file mode 100644 index 00000000..2fa4204c --- /dev/null +++ b/docs/source/tutorials/forall_tutorial.rst @@ -0,0 +1,151 @@ +.. _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. + + +.. 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 head and body are separated by an arrow which means the rule will start evaluating from +timestep ``0``. + +``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). + + +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`` from at timestep ``0`` + - ``Michelle`` views the ``TextMessage`` at timestep ``1`` + - ``Amy`` views the ``TextMessage`` at timestep ``2`` + - ``3`` is the last timestep the rule is active for all. + +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 for three timesteps 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. +This formats the output to display the filtered node and edge data. + + +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``. 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..d52d067b --- /dev/null +++ b/examples/forall_threshold_ex.py @@ -0,0 +1,76 @@ +# Test if the simple program works with thresholds defined +import pyreason as pr +from pyreason import Threshold +import networkx as nx + +# Reset PyReason +pr.reset() +pr.reset_rules() + + +# Create an empty graph +G = nx.DiGraph() + +# Add nodes +nodes = ["TextMessage", "Zach", "Justin", "Michelle", "Amy"] +G.add_nodes_from(nodes) + +# Add edges with attribute 'HaveAccess' +G.add_edge("Zach", "TextMessage", HaveAccess=1) +G.add_edge("Justin", "TextMessage", HaveAccess=1) +G.add_edge("Michelle", "TextMessage", HaveAccess=1) +G.add_edge("Amy", "TextMessage", HaveAccess=1) + + + +# Modify pyreason settings to make verbose +pr.reset_settings() +pr.settings.verbose = True # Print info to screen + +#load the graph +pr.load_graph(G) + +# add custom thresholds +user_defined_thresholds = [ + Threshold("greater_equal", ("number", "total"), 1), + Threshold("greater_equal", ("percent", "total"), 100), + +] + +pr.add_rule( + pr.Rule( + "ViewedByAll(y) <- HaveAccess(x,y), Viewed(x)", + "viewed_by_all_rule", + custom_thresholds=user_defined_thresholds, + ) +) + +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)) + +# Run the program for three timesteps to see the diffusion take place +interpretation = pr.reason(timesteps=3) + +# Display the changes in the interpretation for each timestep +dataframes = pr.filter_and_sort_nodes(interpretation, ["ViewedByAll"]) +for t, df in enumerate(dataframes): + print(f"TIMESTEP - {t}") + print(df) + print() + +assert ( + len(dataframes[0]) == 0 +), "At t=0 the TextMessage should not have been ViewedByAll" +assert ( + len(dataframes[2]) == 1 +), "At t=2 the TextMessage should have been ViewedByAll" + +# TextMessage should be ViewedByAll in t=2 +assert "TextMessage" in dataframes[2]["component"].values and dataframes[2].iloc[ + 0 +].ViewedByAll == [ + 1, + 1, +], "TextMessage should have ViewedByAll bounds [1,1] for t=2 timesteps" From 22588fdb452c701f9e9589a3fd994e8ac86df378 Mon Sep 17 00:00:00 2001 From: Julianna Bucci Date: Fri, 2 Oct 2026 18:31:00 -0400 Subject: [PATCH 2/4] Cleanup after comments --- docs/source/tutorials/forall_tutorial.rst | 28 ++++++++++++++++------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/docs/source/tutorials/forall_tutorial.rst b/docs/source/tutorials/forall_tutorial.rst index 2fa4204c..edef761e 100644 --- a/docs/source/tutorials/forall_tutorial.rst +++ b/docs/source/tutorials/forall_tutorial.rst @@ -4,6 +4,9 @@ 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 statment. +In the example outlined in the tutorial, the groundings of x are the people who hve 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:: @@ -66,11 +69,17 @@ Considering that we only want a text message to be considered viewed by all if i "viewed_by_all_rule", )) -The ``head`` of the rule is ``ViewedByAll(y)`` and the body is ``HaveAccess(x,y), forall(Viewed(x))``. The head and body are separated by an arrow which means the rule will start evaluating from -timestep ``0``. +The ``head`` of the rule is ``ViewedByAll(y)`` and the body is ``HaveAccess(x,y), forall(Viewed(x))``. + +The arrow ``<-`` menas 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 ----- @@ -81,10 +90,10 @@ case they will be immutable later on. Adding PyReason facts gives us more flexib 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`` from at timestep ``0`` + - ``Zach`` and ``Justin`` view the ``TextMessage`` at timestep ``0`` - ``Michelle`` views the ``TextMessage`` at timestep ``1`` - ``Amy`` views the ``TextMessage`` at timestep ``2`` - - ``3`` is the last timestep the rule is active for all. + - Viewed fact holds true until timestep ``3`` . This allows us to see at what timestamp the ``forall(..)`` rule fires. @@ -103,7 +112,7 @@ To run the reasoning in the file: .. code:: python - # Run the program for three timesteps to see the forall(..) function fire + # 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 @@ -114,8 +123,8 @@ To run the reasoning in the file: print(df) print() -This specifies how many timesteps to run for. -This formats the output to display the filtered node and edge data. +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 dataframe entries at each one. Expected output @@ -148,4 +157,7 @@ After running the python file, the expected output is: 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``. + 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. From 08574690505a1f7eba52cff06a1af91c9b1e3e3c Mon Sep 17 00:00:00 2001 From: Julianna Bucci Date: Fri, 2 Oct 2026 18:33:52 -0400 Subject: [PATCH 3/4] Add missing example file --- examples/forall_threshold_ex.py | 95 +++++++++++++-------------------- 1 file changed, 36 insertions(+), 59 deletions(-) diff --git a/examples/forall_threshold_ex.py b/examples/forall_threshold_ex.py index d52d067b..378d4a11 100644 --- a/examples/forall_threshold_ex.py +++ b/examples/forall_threshold_ex.py @@ -1,76 +1,53 @@ -# Test if the simple program works with thresholds defined -import pyreason as pr -from pyreason import Threshold +# 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 -# Reset PyReason -pr.reset() -pr.reset_rules() - - -# 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() +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}), +]) -# Add nodes -nodes = ["TextMessage", "Zach", "Justin", "Michelle", "Amy"] -G.add_nodes_from(nodes) - -# Add edges with attribute 'HaveAccess' -G.add_edge("Zach", "TextMessage", HaveAccess=1) -G.add_edge("Justin", "TextMessage", HaveAccess=1) -G.add_edge("Michelle", "TextMessage", HaveAccess=1) -G.add_edge("Amy", "TextMessage", HaveAccess=1) - - - -# Modify pyreason settings to make verbose -pr.reset_settings() -pr.settings.verbose = True # Print info to screen - -#load the graph +pr.reset() +pr.reset_rules() +pr.settings.verbose = False pr.load_graph(G) - -# add custom thresholds -user_defined_thresholds = [ - Threshold("greater_equal", ("number", "total"), 1), - Threshold("greater_equal", ("percent", "total"), 100), - -] - -pr.add_rule( - pr.Rule( - "ViewedByAll(y) <- HaveAccess(x,y), Viewed(x)", - "viewed_by_all_rule", - custom_thresholds=user_defined_thresholds, - ) -) - +# 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)) -# Run the program for three timesteps to see the diffusion take place interpretation = pr.reason(timesteps=3) -# Display the changes in the interpretation for each timestep +# 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() - -assert ( - len(dataframes[0]) == 0 -), "At t=0 the TextMessage should not have been ViewedByAll" -assert ( - len(dataframes[2]) == 1 -), "At t=2 the TextMessage should have been ViewedByAll" - -# TextMessage should be ViewedByAll in t=2 -assert "TextMessage" in dataframes[2]["component"].values and dataframes[2].iloc[ - 0 -].ViewedByAll == [ - 1, - 1, -], "TextMessage should have ViewedByAll bounds [1,1] for t=2 timesteps" From 490bc266915a666a3e3456d3ad3366388749c6de Mon Sep 17 00:00:00 2001 From: Julianna Bucci Date: Mon, 5 Oct 2026 11:08:05 -0400 Subject: [PATCH 4/4] Cleanup typos --- docs/source/tutorials/forall_tutorial.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/source/tutorials/forall_tutorial.rst b/docs/source/tutorials/forall_tutorial.rst index edef761e..2eadff31 100644 --- a/docs/source/tutorials/forall_tutorial.rst +++ b/docs/source/tutorials/forall_tutorial.rst @@ -4,8 +4,8 @@ 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 statment. -In the example outlined in the tutorial, the groundings of x are the people who hve access to the message. +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. @@ -71,7 +71,7 @@ Considering that we only want a text message to be considered viewed by all if i The ``head`` of the rule is ``ViewedByAll(y)`` and the body is ``HaveAccess(x,y), forall(Viewed(x))``. -The arrow ``<-`` menas the head is inferred in the same timestep the body holds. +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. @@ -124,7 +124,7 @@ To run the reasoning in the file: 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 dataframe entries at each one. +Each pass through this loop will iterate through one timestep and display the data frame entries at each one. Expected output