][git flow]
+
+To create a new feature branch:
+ ```commandline
+ git checkout develop
+ git checkout -b feature/my_branch
+ ```
+
+Please be mindful of existing branches when creating a new branch.
+
+### Pull Requests
+
+1. Use `Black` formatting to ensure that code contributions abide by our code style
+2. Commits should contain one of the following tags before the commit message: `ADD`, `FIX`, `MAINT`
+3. Run `pytest` locally to ensure all changes pass
+
+ NB: All code contributions corresponding to `enhancement` issues should have additional tests accompanying the code changes, located in the `tests/` folder.
+4. Propose your code changes as a `Pull Request DRAFT` that merge into the `develop` branch.
+5. A passed draft can be changed to a formal `Pull Request`.
+6. Add a reviewer to your code so that they can get notified of the proposal - the individual should correspond to the those charged with the yellow tag
+
+### Documentation
+
+LNN documentation can be generated by running `generate_docs.sh` in [docsrc][docsrc] folder.
+
+[docsrc]: https://github.com/IBM/LNN/tree/develop/docsrc
+[git flow]: https://www.atlassian.com/git/tutorials/comparing-workflows/gitflow-workflow
+
+### Handling Circular Imports
+
+A key component in the LNN code base is the `Formula` abstract class. `Formula` is a
+class that refers to itself and the classes that inherit from it. As such, this can lead
+to circular imports. To overcome circular imports we use dictionaries that are keyed
+with the names of the subclasses and the values are the subclasses themselves. These
+dictionaries are populated in the `__init__.py` of the logic module. Thus, when one
+needs to work with a subclass, the subclass can be accessed by passing in the name of
+that subclass to the dictionary. Note that not all classes that inherit from `Formula`
+are added to these dictionaries. Please refer to `__init__.py` if you need to add an
+existing class or new class to one of the dictionaries.
diff --git a/LICENSE b/LICENSE
index 1910215..69fac63 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (C) IBM Corporation 2018-2020
+Copyright (C) IBM Corporation 2018-2022
Apache License
Version 2.0, January 2004
diff --git a/README.md b/README.md
index da371ea..8ef7ce5 100644
--- a/README.md
+++ b/README.md
@@ -1,45 +1,59 @@
-[](https://github.com/IBM/LNN/actions/workflows/build.yml?query=branch%3Amaster)
-[](https://github.com/IBM/LNN/blob/master/LICENSE)
+[](https://github.com/IBM/LNN/blob/master/LICENSE)
+[](https://bestpractices.coreinfrastructure.org/projects/5926)
[](https://github.com/psf/black)
# Logical Neural Networks
-LNNs are a novel `Neuro = symbolic` framework designed to seamlessly provide key
+LNNs are a novel `Neuro = Symbolic` framework designed to seamlessly provide key
properties of both neural nets (learning) and symbolic logic (knowledge and reasoning).
-- Every neuron has a meaning as a component of a formula in a weighted
- real-valued logic, yielding a highly interpretable disentangled representation.
+- Every neuron has a meaning as a component of a formula in a weighted
+ real-valued logic, yielding a highly interpretable disentangled representation.
- Inference is omnidirectional rather than focused on predefined target
variables, and corresponds to logical reasoning, including classical
- first-order logic (FOL) theorem proving as a special case.
-- The model is end-to-end differentiable, and learning minimizes a novel loss
+ first-order logic theorem proving as a special case.
+- The model is end-to-end differentiable, and learning minimizes a novel loss
function capturing logical contradiction, yielding resilience to inconsistent
- knowledge.
+ knowledge.
- It also enables the open-world assumption by maintaining bounds on truth values
- which can have probabilistic semantics, yielding resilience to incomplete
+ which can have probabilistic semantics, yielding resilience to incomplete
knowledge.
## Quickstart
-
To install the LNN:
-1. Run:
- ```
- pip install git+https://github.com/IBM/LNN.git
- ```
-
-To install the LNN with graph plot support:
-1. Install [GraphViz](https://www.graphviz.org/download/)
-2. Run:
- ```
- pip install git+https://github.com/IBM/LNN.git#egg=lnn"[plot]"
- ```
+1. Install [GraphViz](https://www.graphviz.org/download/) and gmp (libgmp3-dev)
+ 
][Docs] | [
][Papers] | [
][Education] | [
][Neuro-Symbolic AI] | [
][API] | [
][Module] |
-
## Citation
If you use Logical Neural Networks for research, please consider citing the
reference paper:
@@ -52,10 +66,9 @@ reference paper:
}
```
-
-[Docs]: https://ibm.github.io/LNN/
-[Papers]: https://ibm.github.io/LNN/papers.html
-[Education]: https://ibm.github.io/LNN/education/education.html
-[API]: https://ibm.github.io/LNN/usage.html
-[Module]: https://ibm.github.io/LNN/lnn/LNN.html
+[Docs]: https://pages.github.com/IBM/LNN/introduction.html
+[Papers]: https://pages.github.com/IBM/LNN/papers.html
+[Education]: https://pages.github.com/IBM/LNN/education/education.html
+[API]: https://pages.github.com/IBM/LNN/usage.html
+[Module]: https://pages.github.com/IBM/LNN/lnn/LNN.html
[Neuro-Symbolic AI]: https://research.ibm.com/teams/neuro-symbolic-ai
diff --git a/docs/.buildinfo b/docs/.buildinfo
index 7f1a5cc..50fb120 100644
--- a/docs/.buildinfo
+++ b/docs/.buildinfo
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 976870eaa406da43ff4c506ff5c2007d
+config: b84c77634a33cf724ade5aeb967569d8
tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/docs/_images/class_diagram.png b/docs/_images/class_diagram.png
index dead73c..647509f 100644
Binary files a/docs/_images/class_diagram.png and b/docs/_images/class_diagram.png differ
diff --git a/docs/_images/raining_implies_wet.png b/docs/_images/raining_implies_wet.png
new file mode 100644
index 0000000..90797f6
Binary files /dev/null and b/docs/_images/raining_implies_wet.png differ
diff --git a/docs/_images/symbolic_class_diagram.png b/docs/_images/symbolic_class_diagram.png
new file mode 100644
index 0000000..9deb953
Binary files /dev/null and b/docs/_images/symbolic_class_diagram.png differ
diff --git a/docs/_modules/index.html b/docs/_modules/index.html
new file mode 100644
index 0000000..790aaf7
--- /dev/null
+++ b/docs/_modules/index.html
@@ -0,0 +1,331 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+##
+# Copyright 2022 IBM Corp All Rights Reserved
+#
+# SPDX-License-Identifier: Apache-20
+##
+
+# flake8: noqa: E501
+
+from enum import Enum, auto
+
+
+class _AutoName(Enum):
+ r"""Automatic enumeration of Enum classes from the variable name.
+
+ The name and value both become str wrapped versions of the given variable
+ e.g. ENUM_VALUE_1 below:
+ ```python
+ MyEnumClass.ENUM_VALUE_1.name = "ENUM_VALUE_1"
+ MyEnumClass.ENUM_VALUE_1.value = "ENUM_VALUE_1"
+ ```
+
+ Examples
+ --------
+
+ ```python
+ class MyEnumClass(_AutoName):
+ ENUM_VALUE_1 = auto()
+ ENUM_VALUE_2 = auto()
+ ENUM_VALUE_3 = auto()
+ ```
+
+ """
+
+ def _generate_next_value_(self, start, count, last_values):
+ return self
+
+
+class _Fact(_AutoName):
+ r"""An enumeration for facts used in state printing."""
+ APPROX_FALSE = auto()
+ APPROX_TRUE = auto()
+ APPROX_UNKNOWN = auto()
+ EXACT_UNKNOWN = auto()
+
+
+class Bound(_AutoName):
+ r"""An enumeration for the Bound of inference.
+
+ Used to restrict an inference to a particular specified bound.
+
+ Parameters
+ ----------
+ LOWER
+ Evaluation of the lower bound of the range, or minimum possible value that truth can take wihtin the given range
+ UPPER
+ Evaluation of the upper bound of the range, or maximum possible value that truth can take wihtin the given range
+
+ """
+ LOWER = auto()
+ UPPER = auto()
+
+
+[docs]class Direction(_AutoName):
+ r"""An enumeration for the direction of inference.
+
+ Used to restrict an inference pass (of a particular node or the entire model) to a single pass of the specified direction.
+
+ Parameters
+ ----------
+ DOWNWARD
+ Evaluation of operands given the operator and the rest of the operands
+ UPWARD
+ Evaluation of the operator given the operands
+
+ """
+ DOWNWARD = auto()
+ UPWARD = auto()
+
+
+[docs]class Fact(Enum):
+ r"""An enumeration for facts.
+
+ Parameters
+ ----------
+ CONTRADICTION
+ A classical interpretation of a contradictory input. Contradictions arise by disagreement of two signal, most often coming from different directions (UPWARD+DOWNWARD). This can be interpreted as a disagreement between the data and the logic, or more appropriately - introducing data to a logic that violates soundness and thereby moves the model into worlds that are not consistent with the logic.
+ FALSE
+ Classically False inputs as represented by LNN bounds
+ TRUE
+ Classically True inputs as represented by LNN bounds
+ UNKNOWN
+ A classical interpretation of what would be an unknown input, this is represented by LNN bounds with complete uncertainty
+
+ """
+ CONTRADICTION = (1.0, 0.0)
+ FALSE = (0.0, 0.0)
+ TRUE = (1.0, 1.0)
+ UNKNOWN = (0.0, 1.0)
+
+
+[docs]class Join(_AutoName):
+ r"""An enumeration for joining methods.
+
+ Parameters
+ ----------
+ INNER : default
+ Extended version of inner db joins that allows groundings to be propagated between operands
+ OUTER
+ Extended outer db join with grounding propagation
+ OUTER_PRUNED
+ A reduced outer join
+
+ """
+ INNER = auto()
+ INNER_EXTENDED = auto()
+ OUTER = auto()
+ OUTER_PRUNED = auto()
+
+
+[docs]class Loss(_AutoName):
+ r"""An enumeration for standard loss functions used during training.
+
+ Parameters
+ ----------
+ CONTRADICTION
+ Ensures logical consistency.
+ CUSTOM
+ Not Implemented.
+ LOGICAL
+ Enforces logical constraints.
+ SUPERVISED
+ Targets [labels](LNN.html#lnn.Model.add_labels).
+ UNCERTAINTY
+ Reduces the uncertainty of bounds.
+
+ """
+ CONTRADICTION = auto()
+ CUSTOM = auto()
+ LOGICAL = auto()
+ SUPERVISED = auto()
+ UNCERTAINTY = auto()
+
+
+[docs]class NeuralActivation(_AutoName):
+ r"""An enumeration of [t-norms](https://en.wikipedia.org/wiki/T-norm#Prominent_examples) for alternate neural computations.
+
+ Used to replace the activation of a connective with the specified activation.
+
+ Parameters
+ ----------
+ Frechet
+ Unweighted [Frechet](https://en.wikipedia.org/wiki/Fr%C3%A9chet_inequalities) - only implemented for propositional logic.
+ Godel
+ Unweighted [Godel](https://en.wikipedia.org/wiki/G%C3%B6del_logic) - only implemented for propositional logic.
+ Lukasiewicz
+ Weighted [Łukasiewicz](https://en.wikipedia.org/wiki/%C5%81ukasiewicz_logic), supported for full first order logic.
+ LukasiewiczTransparent : default
+ Modification of weighted Łukasiewicz that supports learning by allowing identity gradients through the clamped regions.
+ Product
+ Unweighted [Product](https://en.wikipedia.org/wiki/Product_fuzzy_logic) - only implemented for propositional logic.
+
+ """
+ Frechet = auto()
+ Godel = auto()
+ LukasiewiczTransparent = auto()
+ Lukasiewicz = auto()
+ Product = auto()
+
+
+[docs]class World(Enum):
+ r"""An enumeration for world assumptions to for incomplete knowledge.
+
+ See the discussion of [OPEN vs CLOSED](https://en.wikipedia.org/wiki/Open-world_assumption) world assumptions for more information.
+
+ Parameters
+ ----------
+ AXIOM
+ Formulae that follow assumptions of universally being TRUE
+ CONTRADICTION
+ Formulae that are in a contradictory state
+ CLOSED
+ Formulae that follow the closed world assumption
+ FALSE
+ Alias for CLOSED
+ OPEN
+ Formulae that follow the open world assumption
+
+ """
+ AXIOM = (1.0, 1.0)
+ CONTRADICTION = (1.0, 0.0)
+ CLOSED = (0.0, 0.0)
+ FALSE = (0.0, 0.0)
+ OPEN = (0.0, 1.0)
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+import itertools
+from collections.abc import Iterable
+from typing import Union, Dict, Tuple, List
+
+from . import _exceptions, _utils
+from .symbolic._lifted import lifted_axioms
+from .constants import Fact, World, Direction, Join, Loss
+from .symbolic.logic import Proposition, Predicate, Formula
+
+import torch
+import random
+import logging
+import datetime
+import networkx as nx
+from tqdm import tqdm
+import matplotlib.pyplot as plt
+
+_utils.logger_setup(flush=True)
+
+
+[docs]class Model:
+ r"""Creates a container for logical reasoning and neural learning.
+
+ Models define a theory or a collection of formulae, with additional reasoning and
+ learning functionality that can be applied to each formula in the model.
+ In contrast to standard FOL where the existence of a formula symbol assumes a
+ `True` truth value, the data associated with LNN formulae can take on any
+ classical truth (Fact) or belief bounds (a range real-values).
+
+ Models are also dynamic, instantiated as empty containers which are later populated
+ with knowledge rules and data. This additionally allows LNNs to operate in
+ dynamic environments whereby the knowledge acquired may grow as new
+ information becomes available.
+
+ Parameters
+ ------------
+ name : str, optional
+ Name of contextual model, defaults to "Model"
+
+ Attributes
+ ----------
+ graph : nx.DiGraph
+ Directed graph that connects nodes, pointing from operator to operand nodes.
+ nodes : dict
+ Each formula is keyed by a formula_number, with the value as the formula object.
+ query : Formula
+ A formula node that is set as the current query - allows the model to be used in QA/theorem proving whereby inference is governed towards solving the query.
+
+ Examples
+ --------
+ ```python
+ # define the predicates
+ x, y = Variables("x", "y")
+ Smokes, Asthma, Cough = Predicates("Smokes", "Asthma", "Cough")
+ Friends = Predicate("Friends", arity=2)
+
+ # define the connectives/quantifiers
+ Smokers_have_friends = And(Smokes(x), Friends(x, y))
+ Asthmatic_smokers_cough = (
+ Exists(x, Implies(And(Smokes(x), Asthma(x)), Cough(x))))
+ Smokers_befriend_smokers = (
+ ForAll(x, y, Implies(Smokers_have_friends(x, y), Smokes(y))))
+
+ # add root formulae to model
+ model = Model()
+ model.add_knowledge(
+ Asthmatic_smokers_cough,
+ Smokers_befriend_smokers)
+
+ # add data to the model
+ model.add_data({
+ Smokes: {
+ "Person_1": Fact.TRUE,
+ "Person_2": Fact.UNKNOWN,
+ "Person_3": Fact.UNKNOWN},
+ Friends: {
+ ("Person_1", "Person_2"): Fact.TRUE,
+ ("Person_2", "Person_3"): Fact.UNKNOWN}})
+
+ # reason over the model
+ model.infer()
+
+ # verify the model outputs
+ model.print()
+ ```
+
+ """
+
+ def __init__(
+ self,
+ knowledge: Union[Formula, Iterable[Formula]] = None,
+ data: Dict = None,
+ name: str = "Model",
+ ):
+ self.graph = nx.DiGraph()
+ self.nodes = dict()
+ self.node_names = dict()
+ self.node_structures = dict()
+ self.num_formulae = 0
+ self.name = name
+ self.query = None
+ self._converge = None
+ if knowledge:
+ if isinstance(knowledge, Iterable):
+ self.add_knowledge(*knowledge)
+ else:
+ self.add_knowledge(knowledge)
+ if data:
+ self.add_data(data)
+ logging.info(f" {name} {datetime.datetime.now()} ".join(["*" * 22] * 2))
+
+ def __getitem__(
+ self, formula: Union[Formula, int]
+ ) -> Union[Formula, List[Formula]]:
+ r"""Returns a formula object from the model.
+
+ If the formula is in the model, return the formula
+ - for backward compatibility
+ if multiple formula exists in the model with the same structure,
+ return a list of all the relevant nodes
+
+ """
+ if isinstance(formula, int):
+ return self.nodes[formula]
+ if formula.formula_number is not None and formula.formula_number in self.nodes:
+ return self.nodes[formula.formula_number]
+ if formula.structure in self.node_structures:
+ result = self.node_structures[formula.structure]
+ return (
+ result
+ if len(self.node_structures[formula.structure]) > 1
+ else result[0]
+ )
+
+ def __contains__(self, formula: Formula):
+ if formula.formula_number and formula.formula_number in self.nodes:
+ return True
+ return formula.structure in self.node_structures
+
+[docs] def set_query(self, formula: Formula, world=World.OPEN, converge=False):
+ r"""Inserts a query node into the model and maintains a handle on the node.
+
+ Parameters
+ ----------
+ formula : Formula
+ Name of contextual model
+ world : World
+ Default behavior of the formula. If unspecified, assumes open world assumption.
+
+ Notes
+ -----
+ The query formula will be added to the model and will not be removed, even if a new query is defined using this function.
+
+ """
+ self.add_knowledge(formula, world=world)
+ self.query = formula
+ self._converge = converge
+
+[docs] def infer_query(self, *args, **kwds) -> Tuple[Tuple[int, int], torch.Tensor]:
+ r"""Reasons only over the stored query.
+
+ Is the same as calling [model.infer](#lnn.Model.infer) but setting the source
+ node as [model.query](#lnn.Model.set_query)."""
+ if self.query:
+ return self.infer(*args, **kwds, source=self.query)
+
+ def add_formulae(self, *args, **kwds):
+ raise NameError(f"`add_formulae` is deprecated, use `add_knowledge` instead")
+
+[docs] def add_knowledge(self, *formulae: Formula, world: World = None, join: Join = None):
+ r"""Extend the model to include additional formulae.
+
+ Only root level formulae explicitly need to be added to the model.
+ Unless otherwise specified, each root formula follows the open world
+ assumption.
+
+ Examples
+ --------
+ ```python
+ P, Q = Predicates("P1", "Q")
+ model.add_knowledge(P, Q)
+
+ ```
+ creates the predicate and inserts into the model
+
+ or
+
+ ```python
+ model = Model()
+ P1 = Predicate("P1")
+ P2 = Predicate("P2", 2)
+ P3 = Predicate("P3", 3)
+ model.add_knowledge(
+ And(P1(x), P2(x, y)),
+ Implies(P2(x, y), P3(x, y, z))
+ )
+
+ ```
+
+ inserts the formulae roots into the model and appropriately includes
+ all subformulae also into the scope of the model.
+
+ Any formulae that directly require inquiry should first be created in
+ the user scope and thereafter inserted into the model for reference
+ after reasoning/learning
+
+ e.g.
+
+ ```python
+ model = Model()
+ P1 = Predicate("P1")
+ P2 = Predicate("P2", 2)
+ P3 = Predicate("P3", 3)
+ my_and = And(P1(x), P2(x, y))
+ model.add_knowledge(
+ my_and,
+ Implies(P2(x, y), P3(x, y, z))
+ )
+
+ ...
+ model.infer()
+ ...
+
+ my_and.state()
+
+ ```
+
+ """
+ self._add_knowledge(*formulae, world=world, join=join)
+
+ def add_propositions(self, *names: str, **kwds):
+ ret = []
+ for name in names:
+ P = Proposition(name, **kwds)
+ self.add_knowledge(P)
+ ret.append(P)
+ return ret[0] if len(ret) == 1 else ret
+
+ def add_predicates(self, arity: int, *names: str, **kwds):
+ ret = []
+ for name in names:
+ P = Predicate(name, arity=arity, **kwds)
+ self.add_knowledge(P)
+ ret.append(P)
+ return ret[0] if len(ret) == 1 else ret
+
+ def replace_graph_edge(
+ self, old_edge: (Formula, Formula), new_edge: (Formula, Formula)
+ ):
+ self.graph.remove_edge(*old_edge)
+ self.graph.add_edge(*new_edge)
+
+ def _add_knowledge(
+ self, *formulae: Formula, world: World = None, join: Join = None
+ ):
+ for idx, f in enumerate(formulae):
+ _exceptions.AssertFormula(f)
+ self.graph.add_node(f)
+ self.graph.add_edges_from(f.edge_list)
+ self.num_formulae = f.set_formula_number(self.num_formulae) + 1
+ for node in self.graph.nodes:
+ if node.structure in self.node_structures:
+ if node not in self.node_structures[node.structure]:
+ self.node_structures[node.structure].append(node)
+ else:
+ self.node_structures.update({node.structure: [node]})
+ if node.name in self.node_names:
+ if node not in self.node_names[node.name]:
+ self.node_names[node.name].append(node)
+ else:
+ self.node_names.update({node.name: [node]})
+ self.nodes[node.formula_number] = node
+
+ if world:
+ for f in formulae:
+ f.reset_world(world)
+
+ if join:
+ for f in formulae:
+ f.set_join(join)
+
+ def add_facts(self, *args, **kwds):
+ raise NameError(f"`add_facts` is deprecated, use `add_data` instead")
+
+[docs] def add_data(
+ self,
+ data: Dict[
+ Formula,
+ Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ],
+ ):
+ r"""Add data to select formulae in the model, in the form of classical facts or belief bounds.
+
+ Data given is a Fact or belief bounds assumes a propositional formula.
+ Data given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ data : a dict of Fact, belief bounds or dict
+ The dict is keyed by the formula for which data is to be added, with the truths as the value. For propositional formulae, truths are given as either Facts or belief bounds (a tuple of 2 floats). For first-order logic formula, inputs truths are given as a dict. This is further keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P = Proposition("Person")
+ model.add_data({
+ P: Fact.TRUE
+ })
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ BD = Predicate("Birthdate", 2)
+ model.add_data({
+ Person: {
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ },
+ BD: {
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ }
+ })
+ ```
+
+ Warning
+ -------
+ Assumes that the formulae have already been inserted into the model, see [add_knowledge](https://ibm.github.io/LNN/lnn/LNN.html#lnn.Model.add_knowledge) for more details.
+
+ """
+ for formula, fact in data.items():
+ if not isinstance(formula, Formula):
+ raise TypeError(
+ "formula expected of type Formula, received "
+ f"{formula.__class__.__name__}"
+ )
+ _exceptions.AssertFormulaInModel(self, formula)
+ if formula.propositional:
+ _exceptions.AssertBounds(fact)
+ else:
+ _exceptions.AssertFOLFacts(fact)
+ formula.add_data(fact)
+
+[docs] def add_labels(
+ self,
+ labels: Dict[
+ Formula,
+ Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ],
+ ):
+ r"""Add labels to select formulae in the model, in the form of classical facts or belief bounds.
+
+ Labels given is a Fact or belief bounds assumes a propositional formula.
+ Labels given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ labels : a dict of Fact, belief bounds or dict
+ The dict is keyed by the formula for which data is to be added, with the truths as the value. For propositional formulae, truths are given as either Facts or belief bounds (a tuple of 2 floats). For first-order logic formula, inputs truths are given as a dict. This is further keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P = Proposition("Person")
+ model.add_labels({
+ P: Fact.TRUE
+ })
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ BD = Predicate("Birthdate", 2)
+ model.add_labels({
+ Person: {
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ },
+ BD: {
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ }
+ })
+ ```
+
+ Warning
+ -------
+ Assumes that the formulae have already been inserted into the model, see [add_knowledge](https://ibm.github.io/LNN/lnn/LNN.html#lnn.Model.add_knowledge) for more details.
+
+ """
+ for formula, label in labels.items():
+ _exceptions.AssertFormulaInModel(self, formula)
+ if formula.propositional:
+ _exceptions.AssertBounds(label)
+ else:
+ _exceptions.AssertFOLFacts(label)
+ formula.add_labels(label)
+
+ def _traverse_execute(
+ self,
+ func: str,
+ direction: Direction = Direction.UPWARD,
+ source: Formula = None,
+ **kwds,
+ ):
+ r"""Traverse over the model and execute a node operation.
+
+ Traverses through graph from `source` in the given `direction`
+ and execute `func` at each node
+
+ """
+ _exceptions.AssertValidDirection(direction)
+ nodes = None
+ if direction is Direction.UPWARD:
+ nodes = list(nx.dfs_postorder_nodes(self.graph, source))
+ elif direction is Direction.DOWNWARD:
+ nodes = list(reversed(list(nx.dfs_postorder_nodes(self.graph, source))))
+
+ coalesce = torch.tensor(0.0)
+ for node in nodes:
+ val = getattr(node, func)(**kwds) if hasattr(node, func) else None
+ coalesce = coalesce + val if val is not None else coalesce
+ if coalesce and func in [d.value.lower() for d in Direction]:
+ logging.info(f"{direction.value} INFERENCE RESULT:{coalesce}")
+ return coalesce
+
+ def lifted_processing(self, n: Union[float, int]) -> int:
+ axioms = lifted_axioms(self)
+ if len(self.nodes) == 0:
+ logging.debug("no formulae in the model to lift")
+ return 0
+ for _ in range(int(n)):
+ axiom, k = random.choice(list(axioms.items()))
+ if k > len(self.nodes):
+ continue
+ nodes = random.sample(list(self.nodes.values()), k=k)
+ result = int(axiom(*nodes))
+ if result:
+ return result
+ return 0
+
+[docs] def lift(self, lifted: Union[bool, int, float] = True, *args, **kwds):
+ r"""Lift the model without doing bounds-based inference.
+
+ This can be used when a model has TRUE axioms/rules and a query is expected to be answerable directly from the truth of those axioms, i.e. without needing to touch the groundiings/bounds.
+ This uses the LNN as a symbolic manipulation system to introduce new rules based on a set of [axiom schemata](https://en.wikipedia.org/wiki/Propositional_calculus).
+ """
+ self._infer(*args, lifted=lifted, **kwds)
+
+[docs] def infer(
+ self,
+ direction: Direction = None,
+ source: Formula = None,
+ max_steps: int = None,
+ lifted: Union[bool, int, float] = False,
+ **kwds,
+ ) -> Tuple[Tuple[int, int], torch.Tensor]:
+ r"""Reasons over all possible inferences until convergence
+
+ Parameters
+ ----------
+ direction : {Direction.UPWARD, Direction.DOWNWARD}, optional
+ Can be specified as either UPWARD or DOWNWARD inference, a single pass of that direction will be applied. If unspecified, defaults to the LNN naive inference strategy of doing inference until convergence.
+ source : node, optional
+ Specifies starting node for [depth-first search traversal](https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.traversal.depth_first_search.dfs_postorder_nodes.html#networkx.algorithms.traversal.depth_first_search.dfs_postorder_nodes). Specifying a node here will compute reasoning (until convergence) on the subgraph, with the specified source is the root of the subgraph.
+ max_steps: int, optional
+ Limits the inference to a specified number of passes of the naive traversal strategy. If unspecified, the steps will not be limited, i.e. inference will take place until convergence.
+ lifted : bool or float, optional
+ Computes lifted inference processing to modify default truths via the UP/DOWN inference algorithm.
+
+ Returns
+ -------
+ (steps, facts_inferred) : Tuple[tuple of 2 ints, torch.Tensor]
+ The returned `steps` are the number of steps to converge loops, reflecting `lifting steps`, `reasoning steps` accordingly. The `facts_inferred` provide a sum of bounds tightening from inference updates.
+
+ """
+ if lifted:
+ self.lift(lifted)
+
+ return self._infer(
+ direction=direction,
+ source=source,
+ max_steps=max_steps,
+ lifted=False,
+ **kwds,
+ )
+
+ def _infer(
+ self,
+ direction: Direction = None,
+ source: Formula = None,
+ max_steps: int = None,
+ **kwds,
+ ) -> Tuple[Tuple[int, int], torch.Tensor]:
+ r"""Implementation of model inference.
+
+ A model can do inference with lifting, or to explicitly lift without explicitly doing inference (i.e. no bounds updates).
+ `infer` calls `_infer` to do bounds-based inference with/without lifting
+ but `lift` calls `_infer` explicitly without bounds-based inference
+ """
+ direction = (
+ [Direction.UPWARD, Direction.DOWNWARD] if not direction else [direction]
+ )
+ converged, converged_lifting, converged_bounds = False, False, True
+ additional_axioms, steps, facts_inferred = 0, 0, 0
+ lifted = kwds.get("lifted")
+ logging.info(f"{'LIFTED' if lifted else 'BOUNDED'} REASONING LOOP")
+ while not converged:
+ if self.query and self.query.is_classically_resolved and not self._converge:
+ logging.info("=" * 22)
+ logging.info(
+ f"QUERY PROVED AS {self.query.world_state(True)} for "
+ f"'{self.query.name}'"
+ )
+ break
+ logging.info("-" * 22)
+ logging.info(f"REASONING STEP:{steps}")
+ if lifted and converged_bounds is True:
+ is_new_axiom = self.lifted_processing(1e5 if lifted is True else lifted)
+ converged_lifting = True if is_new_axiom == 0 else False
+ additional_axioms += is_new_axiom
+ bounds_diff = 0.0
+ for d in direction:
+ bounds_diff += self._traverse_execute(
+ d.value.lower(), d, source, **kwds
+ )
+ converged_bounds = (
+ True
+ if direction in ([[Direction.UPWARD], [Direction.DOWNWARD]])
+ else bounds_diff <= 1e-7
+ )
+ if converged_bounds:
+ if converged_lifting or not lifted:
+ converged = True
+ else:
+ converged_bounds = True
+ logging.info("NO UPDATES AVAILABLE, TRYING A NEW AXIOM")
+ facts_inferred += bounds_diff
+ steps += 1
+ if max_steps and steps >= max_steps:
+ break
+ logging.info("=" * 22)
+ logging.info(
+ f"INFERENCE CONVERGED WITH {facts_inferred} BOUNDS "
+ f"UPDATES IN {steps} REASONING STEPS "
+ + (f"BY ADDING {additional_axioms} AXIOMS" if lifted else "")
+ )
+ logging.info("*" * 78)
+ return steps, facts_inferred
+
+ def forward(self, *args, **kwds):
+ return self.infer(*args, **kwds)
+
+[docs] def upward(self, **kwds):
+ r"""Performs upward inference for each node in the model from leaf to root."""
+ return self.infer(Direction.UPWARD, **kwds)
+
+[docs] def downward(self, **kwds):
+ r"""Performs downward inference for each node in the model from root to leaf."""
+ return self.infer(Direction.DOWNWARD, **kwds)
+
+[docs] def train(self, losses: Union[Loss, List[Loss], Dict[List[Loss], float]], **kwds):
+ r"""Train the model.
+
+ Reasons across the model until convergence using the standard inference
+ strategy - equivalent to running a NN in the forward direction.
+ At the end of each reasoning pass losses are calculated according to a
+ predefined or custom loss and model parameters are updated.
+ An epoch constitutes all computation until parameters take a step.
+
+ Parameters
+ ------------
+ losses: Loss, list or dict of losses
+ Predefined losses expected from the fixed Loss constants. If given in dict form, coefficients of each loss can be specified as a float value. The value can alternatively specify additional parameters for each loss calculation using a dict.
+ optimizer : pytorch optimizer, optional
+ Custom optimizers should be instantiated with the model parameters using `model.parameters()`. If unspecified, defaults to [Adam](https://pytorch.org/docs/stable/generated/torch.optim.Adam.html#torch.optim.Adam).
+ learning_rate : float, optional
+ If unspecified, defaults to 5e-2.
+ epochs : float, optional
+ Number of training epochs. If unspecified, trains for 3e2 epochs.
+ pbar : bool, optional
+ Prints out a tqdm training progress bar. If unspecified, does not print out.
+
+ Returns
+ -------
+ (epochs, total_loss) : Tuple[int, Tuple[List, Tensor]]
+ A tuple of variables are returned. The `epochs` is number of epochs trained before stopped/converged + 1. The `total_loss` returns a tuple of 2 values: first is the `running_loss` as a list for the sum of loss at the end of each epoch; then the `loss_history`, which is a Tensor of individual loss components as specified by the `losses` argument.
+
+ Examples
+ --------
+ ```python
+ # construct the model from formulae
+ model = Model()
+ p1, p2 = Predicates("P1", "P2")
+ x = Variable("x")
+ AB = And(p1(x), p2(x))
+ model.add_knowledge(AB)
+
+ # add data to the model
+ model.add_data({
+ p1: {
+ "0": Fact.TRUE,
+ "1": Fact.TRUE,
+ '2': Fact.FALSE,
+ '3': Fact.FALSE
+ },
+ p2: {
+ '0': Fact.TRUE,
+ '1': Fact.FALSE,
+ '2': Fact.TRUE,
+ '3': Fact.FALSE,
+ }
+ })
+
+ # add supervisory targets
+ model.add_labels({
+ AB: {
+ '0': Fact.TRUE,
+ '1': Fact.FALSE,
+ '2': Fact.TRUE,
+ '3': Fact.FALSE,
+ }
+ })
+
+ # train the model and output results
+ model.train(losses=Loss.SUPERVISED)
+ model.print(params=True)
+ ```
+
+ """
+ optimizer = kwds.get(
+ "optimizer",
+ torch.optim.Adam(
+ kwds.get("parameters", self.parameters()),
+ lr=kwds.get("learning_rate", 5e-2),
+ ),
+ )
+ running_loss, loss_history, inference_history = [], [], []
+ for epoch in tqdm(
+ range(int(kwds.get("epochs", 3e2))),
+ desc="training epoch",
+ disable=not kwds.get("pbar", False),
+ ):
+ optimizer.zero_grad()
+ if epoch > 0:
+ logging.info(" PARAMETER STEP ".join(["#" * 31] * 2))
+ self.reset_bounds()
+ self.increment_param_history(kwds.get("parameter_history"))
+ _, facts_inferred = self.infer(**kwds)
+ loss_fn = self.loss_fn(losses)
+ loss = sum(loss_fn)
+ if not loss.grad_fn:
+ break
+ if loss and len(loss_fn) > 1:
+ logging.info(f"TOTAL LOSS: {loss}")
+ loss.backward()
+ optimizer.step()
+ self._project_params()
+ running_loss.append(loss.item())
+ loss_history.append([L.clone().detach().tolist() for L in loss_fn])
+ inference_history.append(facts_inferred.item())
+ if loss <= 1e-7 and kwds.get("stop_at_convergence", True):
+ break
+ self.reset_bounds()
+ self.infer()
+ self.increment_param_history(kwds.get("parameter_history"))
+ return (running_loss, loss_history), inference_history
+
+ def parameters(self):
+ result = list(
+ itertools.chain.from_iterable([n.parameters() for n in self.nodes.values()])
+ )
+ return result
+
+ def parameters_grouped_by_neuron(self):
+ result = list()
+ for n in self.nodes.values():
+ param_group = dict()
+ param_group["params"] = list()
+ param_group["param_names"] = list()
+ for name, param in n.named_parameters():
+ param_group["params"].append(param)
+ param_group["param_names"].append(name)
+ param_group["neuron_type"] = n.__class__.__name__
+ result.append(param_group)
+ return result
+
+ def named_parameters(self):
+ result = dict()
+ for n in self.nodes.values():
+ result.update(
+ {f"{n}.{name}": param for name, param in n.named_parameters()}
+ )
+ return result
+
+ def loss_fn(self, losses):
+ if losses is None:
+ raise Exception(
+ "no loss function given, "
+ f"expected losses from the following {[l.name for l in Loss]}"
+ )
+ elif isinstance(losses, Loss):
+ losses = [losses]
+ elif isinstance(losses, list):
+ losses = {c: None for c in losses}
+ result = list()
+ for loss in losses:
+ _exceptions.AssertLossType(loss)
+ if loss == Loss.CUSTOM:
+ if not isinstance(losses[loss], dict):
+ raise TypeError(
+ "custom losses expected as a dict with keys as "
+ "name of the loss and values as function "
+ "definitions"
+ )
+ for loss_fn in losses[loss].values():
+ coalesce = torch.tensor(0.0)
+ for node in list(nx.dfs_postorder_nodes(self.graph)):
+ coalesce = coalesce + loss_fn(node)
+ result.append(coalesce)
+ else:
+ kwds = (
+ losses[loss]
+ if (isinstance(losses[loss], dict))
+ else ({"coeff": losses[loss]})
+ )
+ result.append(
+ self._traverse_execute(f"_{loss.value.lower()}_loss", **kwds)
+ )
+ if result[-1]:
+ logging.info(f"{loss.value.upper()} LOSS {result[-1]}")
+ return result
+
+ def print(
+ self,
+ source: Formula = None,
+ header_len: int = 50,
+ roundoff: int = 5,
+ params: bool = False,
+ grads: bool = False,
+ numbering: bool = False,
+ ):
+ n = header_len + 25
+ print("\n" + "*" * n + f'\n{"":<{n / 2 - 5}}LNN {self.name}\n')
+ self._traverse_execute(
+ "print",
+ Direction.DOWNWARD,
+ source=source,
+ header_len=header_len,
+ roundoff=roundoff,
+ params=params,
+ grads=grads,
+ numbering=numbering,
+ )
+ print("*" * n)
+
+ def plot_graph(
+ self, formula_number: bool = False, edge_variables: bool = False, **kwds
+ ):
+ options = {
+ "with_labels": False,
+ "arrows": False,
+ "edge_color": "#d0e2ff",
+ "node_color": "#ffffff",
+ "node_size": 16,
+ "font_size": 9,
+ }
+ options.update(kwds)
+ pos = nx.drawing.nx_agraph.graphviz_layout(self.graph, prog="dot")
+ nx.draw(self.graph, pos, **options)
+ nx.draw_networkx_labels(
+ self.graph,
+ pos,
+ dict(
+ [
+ (node, node.formula_number)
+ if formula_number
+ else (node, node.connective_str)
+ if hasattr(node, "connective_str")
+ else (node, node.name)
+ for node in self.graph
+ ]
+ ),
+ )
+ if edge_variables:
+ labels = {
+ edge: _utils.list_to_str(
+ edge[0].operand_map[edge[0].operands.index(edge[1])]
+ )
+ for edge in self.graph.edges
+ if isinstance(edge[1], Predicate)
+ }
+ nx.draw_networkx_edge_labels(
+ self.graph,
+ pos,
+ labels,
+ )
+ plt.show()
+
+ def flush(self):
+ self._traverse_execute("flush")
+
+ def reset_bounds(self):
+ self._traverse_execute("reset_bounds")
+
+ def _project_params(self):
+ self._traverse_execute("project_params")
+
+ def increment_param_history(self, parameter_history):
+ if parameter_history:
+ self._traverse_execute(
+ "increment_param_history", parameter_history=parameter_history
+ )
+
+ def has_contradiction(self):
+ return (
+ True
+ if any([node.is_contradiction() for node in self.nodes.values()])
+ else False
+ )
+
+
+##
+# Copyright 2021 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+import logging
+import importlib
+import itertools
+from typing import Optional, Union, Tuple, Iterator, Set, List, Dict, TypeVar
+
+from . import _gm, _trace
+from ._bindings import get_bindings
+from .. import _utils, _exceptions, utils
+from ..constants import Fact, World, Direction, Join, NeuralActivation, Bound
+
+import copy
+import torch
+import numpy as np
+
+_utils.logger_setup()
+
+
+##
+# Internal Classes
+#
+# All classes below are protected classes (denoted with a prefixed underscore)
+# they follow the convention that they will be kept as internal classes rather than
+# exposing them to the end-user as an API.
+# The formulas are ordered according to the inheritance structure in
+# https://ibm.github.io/LNN/lnn/LNN.html
+##
+
+
+[docs]class Formula:
+ r"""Symbolic container for a generic formula.
+
+ Warning
+ -------
+ Formula should not be directly instantiated. The following class is automatically inherited for all formula in the [symbolic hierarchy](LNN.html#symbolic-structure). This class would ordinarily be a protected class but is exposed purely for documentation purposes, i.e., to show all the functionality (attributes and parameters) that is generally available to all instantiated formulae.
+
+ """
+
+ def __init__(
+ self, *formulae: "Formula", name: Optional[str] = "", arity: int = None, **kwds
+ ):
+
+ self.join: Join = kwds.get("join", Join.INNER)
+
+ # construct edge and operand list for each formula
+ self.edge_list = list()
+ self.operands: List[Formula] = list()
+
+ # formula arity
+ self.arity: int = arity
+
+ # inherit propositional, variables, and graphs
+ self.propositional: bool = kwds.get("propositional")
+ self._inherit_from_subformulae(*formulae)
+
+ # formula naming
+ if isinstance(self, _LeafFormula):
+ self.structure: str = name
+ self.name: str = name
+ else:
+ self.structure: str = self._formula_structure(True)
+ self.name: str = (
+ name if name else self._formula_structure(True, lambda x: x.name)
+ )
+
+ # formula grounding table maps grounded objects to table rows
+ self.grounding_table = None if self.propositional else dict()
+
+ # placeholder for neural variables and functions
+ self.neuron = None
+ self.func = None
+ self.func_inv = None
+ self.formula_number = None
+ self.operands_by_number = list()
+ self.congruent_nodes = list()
+
+ ##
+ # External function definitions
+ ##
+
+ def add_facts(self, *args, **kwds):
+ raise NameError(f"`add_facts` is deprecated, use `add_data` instead")
+
+[docs] def add_data(
+ self,
+ data: Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ):
+ r"""Add data to the formula in the form of classical facts or belief bounds.
+
+ Data given is a Fact or belief bounds assumes a propositional formula.
+ Data given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ data : Fact, belief bounds or dict
+ For propositional formulae, truths is given as either Facts or belief bounds (a tuple of 2 floats). For first-order logic formula, inputs truths are given as a dict. It is keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P, Q = Propositions("P", "Q")
+ P.add_data(Fact.TRUE)
+ Q.add_data((.1, .4))
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ Person.add_data({
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ })
+
+ # FOL with arity > 2
+ BD = Predicate("Birthdate", 2)
+ BD.add_data({
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ })
+ ```
+
+ """
+ if self.propositional: # Propositional facts
+ _exceptions.AssertBounds(data)
+ self.neuron.add_data(data)
+
+ else: # FOL facts
+ if isinstance(data, dict): # facts given per grounding
+ # replace fact keys (str -> _Groundings)
+ groundings = tuple(data.keys())
+ for g in groundings:
+ data[self._ground(g)] = data.pop(g)
+
+ # add missing groundings to `grounding_table`
+ groundings = tuple(data.keys())
+ self._add_groundings(*groundings)
+
+ # set facts for all groundings
+ table_facts = {self.grounding_table[g]: data[g] for g in groundings}
+ else:
+ raise Exception(
+ "FOL facts should be from [dict, set], "
+ f'"{self}" received {type(data)}'
+ )
+ self.neuron.add_data(table_facts)
+
+[docs] def add_labels(
+ self,
+ labels: Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ):
+ r"""Store labels as data within the symbolic container.
+
+ Labels given is a Fact or belief bounds assumes a propositional formula.
+ Labels given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ labels : Fact, belief bounds or dict
+ For propositional formulae, facts are given as either Facts or bounds on beliefs (a tuple of 2 floats). For first-order logic formula, inputs are given as a dict. It is keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P, Q = Propositions("P", "Q")
+ P.add_labels(Fact.TRUE)
+ Q.add_labels((.1, .4))
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ Person.add_labels({
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ })
+
+ # FOL with arity > 2
+ BD = Predicate("Birthdate", 2)
+ BD.add_labels({
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ })
+ ```
+
+ """
+ if self.propositional: # Propositional labels
+ _exceptions.AssertBounds(labels)
+ self.labels = _utils.fact_to_bounds(labels, self.propositional)
+
+ else: # FOL labels
+ if not hasattr(self, "labels"):
+ self.labels = dict()
+ if isinstance(labels, dict): # labels given per grounding
+ _labels = copy.copy(labels)
+ for g in tuple(_labels.keys()):
+ # set labels for groundings, replace str keys -> Groundings
+ self.labels[self._ground(g)] = _utils.fact_to_bounds(
+ _labels.pop(g), self.propositional
+ )
+ else:
+ raise Exception(
+ "FOL facts should be from [dict, set], "
+ f'"{self}" received {type(labels)}'
+ )
+
+
+
+ def get_facts(self, *args, **kwds):
+ raise NameError(f"`get_facts` is deprecated, use `get_data` instead")
+
+[docs] def get_data(
+ self, *groundings: Union[str, Tuple[str, ...], "_Grounding"]
+ ) -> torch.Tensor:
+ r"""Returns the current beliefs of the formula.
+
+ Uses the given groundings or the entire `groundind_table` to slice out the
+ current belief bounds from the `bounds_table`.
+
+ Parameters
+ -------
+ ``*groundings``: str or tuple of str
+ NB - if unspecified, defaults to returning all the facts for the given formula. If specified, the table will be ordered according to the input grounding order.
+
+ """
+ if self.propositional or len(groundings) == 0:
+ return self.neuron.get_data()
+ table_rows = list(self.grounding_table.get(self._ground(g)) for g in groundings)
+ if all(row is None for row in table_rows):
+ return torch.Tensor(self.world)
+ result = self.neuron.get_data(table_rows)
+ return result
+
+[docs] def get_labels(self, *groundings: str) -> torch.Tensor:
+ r"""Returns the stored labels from the symbolic container."""
+ if self.propositional or len(groundings) == 0:
+ return self.labels
+ result = torch.stack([self.labels.get(self._ground(g)) for g in groundings])
+ return result[0] if len(groundings) == 1 else result
+
+ @property
+ def groundings(self) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""Returns the groundings to the user as str or tuple of str."""
+ return set(map(_Grounding.eval, self.grounding_table.keys()))
+
+ @property
+ def is_classically_resolved(self):
+ r"""Checks if the query node is in a classical state besides `Fact.UNKNOWN`."""
+ if self.propositional and _utils.is_classical_proposition(
+ tuple(self.get_data().tolist())
+ ):
+ return True
+ return False
+
+[docs] def is_contradiction(
+ self, bounds: torch.Tensor = None, stacked=False
+ ) -> torch.BoolTensor:
+ r"""Check if bounds are in contradiction."""
+ if stacked:
+ result = any(
+ [self.neuron.is_contradiction(bounds[..., dim]).any() for dim in [0, 1]]
+ )
+ else:
+ result = self.neuron.is_contradiction(bounds).any()
+ return result
+
+[docs] def is_equal(self, other: "Formula") -> bool:
+ r"""Returns True if two nodes are symbolically equivalent.
+
+ Formulae can be symbolically equivalent yet neurally different, example:
+ ```python
+ f = And(A, B, activation={"type": NeuralActivation.Lukasiewicz})
+ g = And(A, B, activation={"type": NeuralActivation.Godel})
+ ```
+ The above will return `True`, since `f` is symbolically equivalent to `g`
+ despite different neural configurations.
+
+ """
+ if self is other:
+ return True
+ result = list()
+ for f in self.congruent_nodes:
+ if isinstance(f, Congruent):
+ result += [
+ other.structure == operand.structure for operand in f.operands
+ ]
+ return any(result)
+
+ def is_unweighted(self) -> bool:
+ return all([self.neuron.bias == w for w in self.neuron.weights])
+
+ def negation_absorption(
+ self, store: bool = True
+ ) -> (List[int], Tuple[Tuple["Formula"]]):
+ n_negations = []
+ edge_replace = []
+ operands = []
+
+ def recurse(formula):
+ for operand in formula.operands:
+ if isinstance(operand, Not):
+ recurse(operand)
+ root_idx = len(n_negations) - 1
+ n_negations[root_idx] += 1
+ condition = [True] * len(self.neuron.weights)
+ condition[root_idx] = bool(root_idx % 2)
+ if store:
+ self.neuron.update_weights_where(
+ condition, -self.neuron.weights
+ )
+ self.operands[root_idx] = self.operands[root_idx].operands[0]
+ edge_replace.append(
+ (self.edge_list[root_idx], (self, self.operands[root_idx]))
+ )
+ else:
+ n_negations.append(0)
+ operands.append(operand)
+
+ recurse(self)
+ if store:
+ if edge_replace:
+ logging.info(f"ABSORBED NEGATIONS INTO WEIGHTS FOR: '{self.name}'")
+ return edge_replace, n_negations
+ else:
+ return operands, edge_replace, n_negations
+
+ def named_parameters(self) -> Iterator[Tuple[str, torch.Tensor]]:
+ yield from self.neuron.named_parameters()
+
+ def parameters(self) -> Iterator[torch.Tensor]:
+ for name, param in self.neuron.named_parameters():
+ yield param
+
+ def params(
+ self, *params: str, detach: bool = False
+ ) -> Union[torch.Tensor, List[torch.Tensor]]:
+ result = list()
+ for param in params:
+ if param in dict(self.neuron.named_parameters()):
+ result.append(
+ getattr(self.neuron, param).clone().detach()
+ if detach
+ else getattr(self.neuron, param)
+ )
+ else:
+ raise ValueError(f"{self} has no attribute: {param}")
+ return result[0] if len(params) == 1 else result
+
+[docs] def print(
+ self,
+ header_len: int = 50,
+ roundoff: int = 5,
+ params: bool = False,
+ grads: bool = False,
+ numbering: bool = False,
+ ):
+ r"""Print the states of groundings in a formula.
+
+ ```
+ OPEN Proposition: A UNKNOWN (L, U)
+
+ CLOSED Proposition: B FALSE (L, U)
+
+ OPEN Predicate: P1 (x)
+ "const_1" TRUE (L, U)
+ "const_2" CONTRADICTION (L, U)
+ "const_3" FALSE (L, U)
+
+ OPEN Predicate: P2 (x, y)
+ ("const_1", "const_5") TRUE (L, U)
+ ("const_2", "const_6") CONTRADICTION (L, U)
+ ("const_3", "const_7") FALSE (L, U)
+
+ OPEN And: And_0 (x, y)
+ Bindings: P1 (x: "const_1"), P2 (x: 'const_2', y: ['const_3', ...])
+ ('const_1', 'const_3') TRUE (L, U)
+ ('const_2', 'const_3') CONTRADICTION (L, U)
+ ('const_1', 'const_7') FALSE (L, U)
+
+ TRUE ForAll: ForAll_0 (y) UNKNOWN (L, U)
+ ```
+
+ """
+
+ def state_wrapper(grounding: _Grounding):
+ return (
+ f"'{grounding}'" if grounding.grounding_arity == 1 else f"{grounding}"
+ )
+
+ def round_bounds(grounding=None):
+ return tuple(
+ [
+ round(r, roundoff)
+ for r in (
+ self.get_data(grounding)
+ if self.propositional
+ else self.get_data(grounding)[0]
+ ).tolist()
+ ]
+ )
+
+ header = (
+ f"{str(self.world_state(True))} "
+ f"{self.__class__.__name__}"
+ f": {self.name}"
+ )
+ if params:
+ params = dict()
+ for name, symbol in _utils.param_symbols.items():
+ if hasattr(self.neuron, name):
+ val = getattr(self.neuron, name)
+ params[symbol] = f"{np.around(val.tolist(), roundoff)}" + (
+ f" grads {np.around(val.grad.tolist(), roundoff)}"
+ if grads and val.grad is not None
+ else ""
+ )
+ params = "params " + ", ".join([f"{k}: {v}" for k, v in params.items()])
+ else:
+ params = ""
+ number = (
+ f"{self.formula_number} {self.operands_by_number}: "
+ if self.formula_number is not None and numbering
+ else ""
+ )
+
+ # print propositional node - single bounds
+ if self.propositional:
+ states = (
+ f"{header:<{header_len}} "
+ f"{self.state().name:>13} "
+ f"{round_bounds()}\n"
+ f"{params}"
+ )
+ print(f"{number}{states}")
+
+ # print FOL node - table of bounds
+ else:
+ facts = (
+ [""]
+ if self.grounding_table is None
+ else (
+ [
+ (
+ f"{state_wrapper(g):{header_len}} "
+ f"{self.state(g).name:>13} "
+ f"{round_bounds(g)}\n"
+ )
+ for g in self.grounding_table
+ ]
+ )
+ )
+ binder = list()
+ for op_idx, op in enumerate(self.operands):
+ if not self.propositional and self._has_bindings(op_idx):
+ for i in range(len(self.var_remap[op_idx])):
+ if None not in self.bindings[op_idx][i]:
+ binder.append(
+ f"{str(op)} "
+ "{"
+ f"{str(self.operand_map[op_idx][i])}: "
+ f"{list(map(str, self.bindings[op_idx][i]))}"
+ "}"
+ )
+ bind_str = ("\nBindings: " + ", ".join(binder)) if binder else ""
+ header = f"{header} {bind_str}"
+ params = f"\n{params}" if params else ""
+ header = f"{header}{params}"
+ result = f"{header}\n" + "".join(facts)
+ print(f"{number}{result}")
+
+ def project_params(self):
+ self.neuron.project_params()
+
+ def rename(self, name: str):
+ self.name = name
+
+ def reset_bounds(self):
+ self.neuron.reset_bounds()
+
+ def reset_world(self, world: World):
+ _exceptions.AssertBoundsLen(world)
+ self.world = world if isinstance(world, tuple) else world.value
+ self.neuron.reset_world(world)
+
+ def set_formula_number(self, idx) -> int:
+ self.formula_number = idx
+ for operand in self.operands:
+ if operand.formula_number is None:
+ idx = operand.set_formula_number(idx + 1)
+ self.operands_by_number.append(operand.formula_number)
+ return idx
+
+ def set_join(self, join: Join):
+ _exceptions.AssertJoin(join)
+ self.join = join
+
+[docs] def set_negative_weights(
+ self, is_negative: bool = True, store: bool = True
+ ) -> (List[int], Tuple[Tuple["Formula"]]):
+ """absorb `Not` into weights and allow negative computation"""
+ self.neuron.set_negative_weights(is_negative)
+ return self.negation_absorption(store=store)
+
+[docs] def set_propositional(self, propositional: bool):
+ r"""Set's the neuron's world parameter."""
+ self.propositional = propositional
+
+ @property
+ def shape(self) -> torch.Size:
+ return self.neuron.bounds_table.shape
+
+[docs] def state(
+ self,
+ groundings: Union[
+ str, Tuple[str, ...], List[str], List[Tuple[str, ...]]
+ ] = None,
+ to_bool: bool = False,
+ bounds: torch.Tensor = None,
+ ) -> Union[torch.Tensor, Dict[Union[str, Tuple[str, ...]], torch.Tensor]]:
+ r"""Returns the state of a single grounded fact.
+
+ Parameters
+ ----------
+ groundings : groundings, optional
+ If unspecified, will return the state of all groundings.
+ bounds: torch.Tensor, optional
+ Forces the function to return the state of the given tensor. If unspecified, will return the bounds tensor currently stored in the node.
+ to_bool : bool, optional.
+ If to_bool flag is True, will map classical Facts to bool: i.e. {Fact.True: True, FALSE': False}. The states that cannot be converted to bool will return as str, e.g. `'APPROX_TRUE'`. If unspecified, will not convert to bool.
+
+ Notes
+ -----
+ see section [F.2](https://arxiv.org/abs/2006.13155) for more
+ information on node states
+
+ """
+ if self.propositional:
+ result = self.neuron.state()
+ else:
+ if bounds is None:
+ if groundings is None or isinstance(groundings, list):
+ result = {
+ str(g): self.state(g)
+ for g in (
+ self.grounding_table if groundings is None else groundings
+ )
+ }
+ return result
+ groundings = self._ground(groundings)
+ bounds = self.get_data(groundings)
+ if len(bounds) == 0:
+ raise LookupError(f"grounding {groundings} not found in {str(self)}")
+ result = self.neuron.state(bounds[None, :])[0]
+ result = _utils.node_state(result)
+ return utils.fact_to_bool(result) if to_bool else result
+
+ @property
+ def variable_slots(self) -> Dict:
+ result = {u: i for i, u in enumerate(self.unique_vars)}
+ if isinstance(self, _Quantifier):
+ for idx, v in enumerate(self.variables):
+ result[v] = idx + len(self.unique_vars)
+ return result
+
+ @property
+ def world(self) -> World:
+ r"""Proxy to get the neuron's world parameter."""
+ return self.neuron.world
+
+ @world.setter
+ def world(self, new_world: Union[Tuple, World]):
+ r"""Proxy to set the neuron's world parameter."""
+ self.neuron.world = new_world
+
+[docs] def world_state(self, name=False):
+ r"""Returns the state of the `world` variable."""
+ try:
+ w = World(self.world)
+ return w.name if name else w
+ except ValueError:
+ return self.world
+
+ def And(self, *formulae: "Formula", **kwds) -> "And":
+ return And(*self._formula_vars(self, *formulae), **kwds)
+
+ def Or(self, *formulae: "Formula", **kwds) -> "Or":
+ return Or(*self._formula_vars(self, *formulae), **kwds)
+
+ def Implies(self, formula: "Formula", **kwds) -> "Implies":
+ return Implies(*self._formula_vars(self, formula), **kwds)
+
+ def Not(self, **kwds) -> "Not":
+ return Not(*self._formula_vars(self), **kwds)
+
+ def Equivalent(self, formula: "Formula", **kwds) -> "Equivalent":
+ return Equivalent(*self._formula_vars(self, formula), **kwds)
+
+ def Exists(self, **kwds) -> "Exists":
+ return Exists(self.unique_vars, self, **kwds)
+
+ def ForAll(self, **kwds) -> "ForAll":
+ return ForAll(*self.unique_vars, self, **kwds)
+
+ ##
+ # Internal function definitions
+ ##
+
+ CalledFormula = TypeVar(
+ "CalledFormula",
+ bound=Union[
+ Tuple[
+ "Formula",
+ Tuple["Variable", ...],
+ Tuple["Variable", ...],
+ Union[None, List[Union[List["_Grounding"], List[None]]]],
+ ],
+ ],
+ )
+
+ def __call__(
+ self,
+ *variables: "Variable",
+ bind: Dict["Variable", Union[str, List[str]]] = None,
+ ) -> CalledFormula:
+ r"""Variable remapping between operator and operand variables.
+
+ Examples
+ --------
+ FOL formulae that appear in connectives are callable:
+ Note `A`, `B` in the `And`
+ ```python
+ x = Variable('x')
+ model['A'] = Predicate('A')
+ model['B'] = Predicate('B')
+ model['AB'] = And(A(x), B(x))
+ ```
+
+ Returns
+ -------
+ Formula:
+ reference to the child object
+ variables:
+ tuple of child's Variables
+ var_remap:
+ tuple of parent-to-child remapping Variables
+ bindings:
+ tuple of parent-to-child groundings to bind inference to single groundings are _Grounding multiple groundings are list(_Grounding)
+
+ """
+ if len(variables) != self.num_unique_vars:
+ raise Exception(
+ f"please check if the FOL arity of {self} is correctly set for the "
+ f"number of variables, length ({len(variables)}) must be the same "
+ f"length as `num_unique_vars` ({self.num_unique_vars})"
+ )
+ bindings = list()
+ if bind is None:
+ bind = dict()
+ for v in variables:
+ if not isinstance(v, Variable):
+ raise TypeError(f"expected variable, received {type(v)}")
+ if v in bind: # extract bindings
+ if isinstance(bind[v], str): # a single binding
+ bindings.append([self._ground(bind[v], arity_match=False)])
+ elif isinstance(bind[v], list): # multiple bindings
+ bindings.append(
+ [self._ground(g, arity_match=False) for g in bind[v]]
+ )
+ elif isinstance(bind[v], Function): # A single function
+ bindings.append([bind[v]])
+ elif isinstance(bind[v], tuple): # A bound function
+ bindings.append([bind[v]])
+ else:
+ raise TypeError(
+ f"bindings expected as str, "
+ f"Function or list of str or "
+ f"Function, received {type(bind[v])}"
+ )
+ else:
+ bindings.append([None])
+ return self, self.unique_vars, variables, bindings
+
+ def __str__(self) -> str:
+ return self.name
+
+ def _add_groundings(self, *groundings: "_Grounding"):
+ r"""Adds missing groundings to `grounding_table` for those not yet stored.
+
+ Examples
+ --------
+ ```python
+ # for formulae with arity == 1:
+ formula._add_groundings(_Grounding_1, _Grounding_2)
+ ```
+ ```python
+ # for formulae with arity > 1:
+ groundings = ((_Grounding_1, _Grounding_7),
+ (_Grounding_2, _Grounding_8))
+ formula._add_groundings(*groundings)
+ ```
+
+ Warning
+ -------
+ groundings must be given in grounded form: `self._ground(grounding)`
+
+ """
+ missing_groundings = {g for g in groundings if g not in self.grounding_table}
+ if len(missing_groundings) == 0:
+ self._has_new_groundings = False
+ return
+ self._has_new_groundings = True
+ table_rows = self.neuron.extend_groundings(len(missing_groundings))
+ self.grounding_table.update(
+ {g: table_rows[i] for i, g in enumerate(missing_groundings)}
+ )
+
+ def _formula_structure(self, as_int, get_str=lambda x: x.structure) -> str:
+ r"""Determine a name for input formula(e)."""
+
+ def subformula_structure(
+ subformula: Formula,
+ operator: str = None,
+ subformula_vars: Tuple = None,
+ root_var_remap: dict = None,
+ ) -> str:
+ if subformula_vars is None:
+ root_var_remap = dict(
+ (k, k)
+ for k in (
+ self.expanded_unique_vars
+ if isinstance(self, _Quantifier)
+ else self.unique_vars
+ )
+ )
+ else:
+ if isinstance(subformula, _Quantifier):
+ for v in subformula.expanded_unique_vars:
+ if v not in root_var_remap:
+ root_var_remap[v] = v
+ if subformula_vars != subformula.unique_vars:
+ root_var_remap = dict(
+ (
+ (
+ subformula.unique_vars[i],
+ root_var_remap[subformula_vars[i]],
+ )
+ if subformula.unique_vars[i] != subformula_vars[i]
+ else (subformula_vars[i], subformula_vars[i])
+ for i in range(len(subformula_vars))
+ )
+ )
+ result = [
+ (
+ f"{f.name}("
+ + _utils.list_to_str(
+ [
+ root_var_remap[v]
+ if not as_int
+ else subformula.variable_slots[root_var_remap[v]]
+ if isinstance(subformula, _Quantifier)
+ else self.variable_slots[root_var_remap[v]]
+ for v in [
+ subformula.expanded_unique_vars[_]
+ if isinstance(subformula, _Quantifier)
+ else subformula.unique_vars[_]
+ for _ in subformula.operand_map[i]
+ ]
+ ]
+ )
+ + ")"
+ )
+ if isinstance(f, Predicate)
+ else f"({f.structure})"
+ if isinstance(f, _Quantifier)
+ else (
+ "("
+ + subformula_structure(
+ f, f.operator_str, subformula.var_remap[i], root_var_remap
+ )
+ + ")"
+ )
+ if isinstance(f, _ConnectiveNeuron)
+ else (
+ f"{f.operator_str}"
+ + subformula_structure(
+ f, None, subformula.var_remap[i], root_var_remap
+ )
+ )
+ if isinstance(f, Not)
+ else ""
+ for i, f in enumerate(subformula.operands)
+ ]
+ return f" {operator} ".join(result) if operator else "".join(result)
+
+ if isinstance(self, _Quantifier):
+ return (
+ f"({self.operator_str}{self.quantified_variable}, "
+ f"{subformula_structure(self)})"
+ )
+
+ elif isinstance(self, Not):
+ return (
+ f"{self.operator_str}{get_str(self.operands[0])}"
+ if self.propositional
+ else f"{self.operator_str}{subformula_structure(self)}"
+ )
+ return (
+ (
+ "("
+ + f" {self.operator_str} ".join([get_str(f) for f in self.operands])
+ + ")"
+ )
+ if self.propositional
+ else f"({subformula_structure(self, self.operator_str)})"
+ )
+
+ @staticmethod
+ def _formula_vars(*formulae: "Formula") -> List[Union["Formula", Tuple]]:
+ r"""Returns a list of formulae as wither called (when predicates)
+ or uncalled as connectives.
+ """
+ variables = list(
+ Variable(f"?{i}") for i in range(max([f.arity for f in formulae]))
+ )
+ return [
+ f(*variables[: f.arity])
+ if (not f.propositional and isinstance(f, Predicate))
+ else f
+ for f in formulae
+ ]
+
+ def _ground(
+ self,
+ grounding: Union[str, Tuple[str, ...], "_Grounding"],
+ arity_match: bool = True,
+ ) -> "_Grounding":
+ r"""Returns a single grounded object given a grounding in str form.
+
+ If the grounding is already an internal "Grounding" object, it will simply be
+ returned to the user as is.
+
+ Examples
+ --------
+ ```python
+ # for arity == 1
+ self._ground('str_1')
+ ```
+ ```python
+ # for arity > 1
+ grounding = ('str_1', 'str_2', ...)
+ self._ground(grounding)
+ ```
+
+ Warning
+ -------
+ This function can only ground one object at a time due to tuple confusion
+ for multiple objects
+
+ """
+ if Formula._is_grounded(grounding):
+ return grounding
+ if isinstance(grounding, tuple):
+ if not all([type(g) in [str, None] for g in grounding]):
+ raise Exception(
+ "expected groundings as tuple of str for num_unique_vars "
+ f" > 1, received {type(grounding)} {grounding}"
+ )
+ if len(grounding) != self.num_unique_vars and arity_match:
+ raise Exception(
+ "expected grounding length to be of "
+ f"arity {self.num_unique_vars}, received {grounding}"
+ )
+ else:
+ if self.num_unique_vars != 1 and arity_match:
+ raise Exception(
+ f"{self} received str as grounding, expected grounding "
+ f"({grounding}) as a tuple of len {self.num_unique_vars}"
+ )
+ return _Grounding(grounding)
+
+ def _ground_functions(self):
+ r"""Grounds a "Function" if given bindings that are fully bound."""
+ tmp_bindings = [tuple([get_bindings(g) for g in op]) for op in self.bindings]
+
+ for op_id, op in enumerate(self.operands):
+
+ # If there are groundings and partial bindings we can still
+ # create new groundings by combining the partials from
+ # groundings and bindings. But we need the ability
+ # to extract partial groundings without the grounding string.
+ #
+ # ```python
+ # bindings = [g for g in product(*tmp_bindings[op_id])]
+ # for g in op.groundings: # Tuple
+ # for binding in bindings:
+ # new_g = [g[b] if binding[b] is None else binding[b]
+ # for b in range(len(binding))]
+ # op._add_groundings(tuple(new_g))
+ # ```
+
+ if all([False if g[0] is None else True for g in tmp_bindings[op_id]]):
+ for g in itertools.product(*tmp_bindings[op_id]):
+ if len(g) == 1:
+ op._add_groundings(op._ground(g[0]))
+ else:
+ op._add_groundings(op._ground(g))
+
+ @property
+ def _groundings(self) -> Set["_Grounding"]:
+ """Internal usage to extract groundings as _Grounding object"""
+ return set(self.grounding_table.keys())
+
+ def _has_bindings(self, slot: int = None) -> bool:
+ r"""Returns True if Formula has any bindings."""
+ if isinstance(slot, int):
+ return (
+ True
+ if any(
+ [
+ self.bindings[slot][i][j]
+ for i in range(len(self.bindings[slot]))
+ for j in range(len(self.bindings[slot][i]))
+ ]
+ )
+ else False
+ )
+ return any([self._has_bindings(i) for i in range(len(self.bindings))])
+
+ def _inherit_from_subformulae(self, *subformula: Union["Formula", Tuple]):
+ r"""Builds the local context for a formula using subformulae.
+
+ provides manual manual variable remapping if given with variables:
+ i.e. Formula used as a function via `__call__`
+ alternatively inherits remapping from operands if formula is not called
+
+ """
+
+ # inheritance variables
+ subformulae = list()
+ _operand_vars: List[Union[Tuple["Variable", ...], None]] = [None] * self.arity
+ _var_remap: List[Union[Tuple["Variable", ...], None]] = [None] * self.arity
+ _bindings: List[Union[Tuple[_Grounding, ...], None]] = [None] * self.arity
+
+ for slot, f in enumerate(subformula):
+
+ # variable remapping from CalledFormula:
+ #
+ # ```python
+ # P = Predicate("P", arity=2)
+ # Q = Predicate("P", arity=2)
+ # And(P(x, y), Q(y, z))
+ # ```
+ if isinstance(f, tuple):
+ subformulae.append(f[0])
+ _operand_vars[slot] = f[1]
+ _var_remap[slot] = f[2]
+ _bindings[slot] = f[3]
+
+ self.edge_list.append((self, f[0]))
+ self.operands.append(f[0])
+
+ # automatically inherit variable remapping from `uncalled` operands
+ # for higher level connective formulae:
+ #
+ # ```python
+ # Implies(And(...), Or(...))
+ # ```
+ else:
+ if not f.propositional:
+ _operand_vars[slot] = f.unique_vars
+ _var_remap[slot] = f.unique_vars
+ _bindings[slot] = [[None]] * len(f.unique_vars)
+ subformulae.append(f)
+
+ self.edge_list.append((self, f))
+ self.operands.append(f)
+ self.operands: Tuple[Formula] = tuple(self.operands)
+
+ # set class variables as read-only tuples
+ self.operand_vars: Tuple[Tuple["Variable", ...], ...] = tuple(_operand_vars)
+ self.var_remap: Tuple[Tuple["Variable", ...], ...] = tuple(_var_remap)
+ self.bindings: Tuple[Tuple[_Grounding, ...], ...] = tuple(_bindings)
+
+ # inherit propositional flag from children
+ if self.propositional is None:
+ self.set_propositional(
+ False if any([not f.propositional for f in subformulae]) else True
+ )
+
+ # remap the FOL formula if its called
+ #
+ # ```python
+ # Implies(And(...)(u, v), Or(...)(u, v))
+ # ```
+ if not self.propositional and not isinstance(self, _LeafFormula):
+ self._update_variables(*self.var_remap)
+ self._update_map()
+
+ # expand formula graph to include all subformulae
+ if subformulae:
+ self.edge_list.extend([edge for f in subformulae for edge in f.edge_list])
+
+ @staticmethod
+ def _is_grounded(groundings: Union["_Grounding", str, Tuple[str, ...]]) -> bool:
+ r"""Returns True if the grounding is given in internal "Grounded" form."""
+ return isinstance(groundings, _Grounding)
+
+ @staticmethod
+ def _get_unique_variables(*variables: Tuple["Variable", ...]) -> Tuple:
+ r"""Combines all predicate variables into a unique tuple
+ the tuple is sorted by the order of appearance of variables in
+ the operands.
+ """
+ result = list()
+ for op_vars in variables:
+ for v in op_vars:
+ if v not in result:
+ result.append(v)
+ return tuple(result)
+
+ def _update_map(self):
+ r"""Update the 'operand_map' to map parent variables to operand variables.
+
+ Attributes
+ ----------
+ `operand_map`: Tuple[Tuple[int, ...]]
+ tells you which slots the parent variable will appear in the children variables.
+ """
+ self.operand_map: List = [None] * len(self.operand_vars)
+ for op_idx in range(len(self.var_remap)):
+ op_map = [
+ self.unique_vars.index(op_var)
+ for op_var in self.var_remap[op_idx]
+ if op_var in self.unique_vars
+ ]
+ self.operand_map[op_idx] = tuple(op_map)
+ self.operand_map: Tuple[Tuple[int, ...]] = tuple(self.operand_map)
+
+ def _update_variables(self, *variables: Tuple["Variable", ...]):
+ r"""
+ **Notes**
+
+ If the formula grounding_arity is not specified, it will be inherited
+ from the variables. If variables are not specified, both the
+ `grounding_arity` and variables are inherited from groundings
+
+ """
+
+ self.unique_vars = Formula._get_unique_variables(*variables)
+ self.num_unique_vars = len(self.unique_vars)
+
+ def _contradiction_loss(self, coeff: float = None) -> torch.Tensor:
+ r"""Contradiction loss."""
+ if coeff is None:
+ coeff = 1
+ bounds = self.get_data()
+ x = bounds[..., 0] - bounds[..., 1]
+ return (self.is_contradiction() * coeff * x).sum()
+
+ def _uncertainty_loss(self, coeff: float = None) -> torch.Tensor:
+ r"""Uncertainty loss."""
+ if coeff is None:
+ coeff = 0
+ bounds = self.get_data()
+ x = bounds[..., 1] - bounds[..., 0]
+ return (self.is_contradiction().logical_not() * coeff * x).sum()
+
+ def _supervised_loss(self, coeff: float = None) -> Union[None, torch.Tensor]:
+ r"""Supervised loss."""
+ if coeff is None:
+ coeff = 1
+ loss = torch.nn.MSELoss()
+ if (
+ not hasattr(self, "labels")
+ or (self.propositional and not self.labels.numel())
+ or (not self.propositional and not self.labels)
+ ):
+ return
+ labels = self.get_labels()
+ if self.propositional:
+ return coeff * loss(self.get_data(), labels)
+ groundings = [g for g in labels if g in self.grounding_table]
+ if len(groundings) == 0:
+ return
+ return coeff * loss(self.get_data(*groundings), self.get_labels(*groundings))
+
+ increment_param_history = _trace.increment_param_history
+
+
+class _LeafFormula(Formula):
+ r"""Specifies activation functionality as nodes instead of neurons.
+
+ Assumes that all leaf formulae are propositions or predicates, therefore
+ uses the _NodeActivation accordingly
+
+ """
+
+ def __init__(self, *args, **kwds):
+ super().__init__(*args, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+
+class _ConnectiveFormula(Formula):
+ def __init__(self, *formula: Formula, **kwds):
+ super().__init__(*formula, **kwds)
+
+
+class _ConnectiveNeuron(_ConnectiveFormula):
+ def __init__(self, *formula, **kwds):
+ super().__init__(*formula, **kwds)
+ kwds.setdefault("arity", self.arity)
+ kwds.setdefault("propositional", self.propositional)
+ if kwds.get("activation", {}).get("negative_weights"):
+ self.negation_absorption()
+ self.neuron = _NeuralActivation(kwds.get("activation", {}).get("type"))(
+ **kwds.get("activation", {}), **kwds
+ )
+ self.func = self.neuron.activation(
+ self.__class__.__name__, direction=Direction.UPWARD
+ )
+ self.func_inv = self.neuron.activation(
+ self.__class__.__name__, direction=Direction.DOWNWARD
+ )
+
+ def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = self.neuron.aggregate_world(
+ tuple(
+ self.func(
+ torch.stack(
+ [torch.tensor(op.world) for op in self.operands], dim=-1
+ )[None]
+ ).tolist()[0]
+ )
+ )
+ if result:
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ upward_bounds = _gm.upward_bounds(self, self.operands, groundings)
+ if upward_bounds is None: # contradiction arresting
+ return 0.0
+ input_bounds, groundings = upward_bounds
+ grounding_rows = (
+ None
+ if self.propositional
+ else (
+ self.grounding_table.values()
+ if groundings is None
+ else [self.grounding_table.get(g) for g in groundings]
+ )
+ )
+ result = self.neuron.aggregate_bounds(
+ grounding_rows, self.func(input_bounds)
+ )
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ if self.is_contradiction():
+ logging.info(
+ "↑ CONTRADICTION "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+ def downward(
+ self,
+ index: int = None,
+ groundings: Set[Union[str, Tuple[str, ...]]] = None,
+ **kwds,
+ ) -> float:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ index : int, optional
+ restricts downward inference to an operand at the specified index. If unspecified, all operands are updated.
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = 0.0
+ new_worlds = self.func_inv(
+ torch.tensor(self.world)[None],
+ torch.stack([torch.tensor(op.world) for op in self.operands], dim=-1)[
+ None
+ ],
+ )
+ for op_idx, op in enumerate(self.operands):
+ op_aggregate = op.neuron.aggregate_world(
+ tuple(new_worlds[..., op_idx].tolist()[0])
+ )
+ result += op_aggregate
+ if op_aggregate:
+ logging.info(
+ "↓ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ else:
+ downward_bounds = _gm.downward_bounds(self, self.operands, groundings)
+ if downward_bounds is None: # contradiction arresting
+ return 0.0
+ out_bounds, input_bounds, groundings = downward_bounds
+ new_bounds = self.func_inv(out_bounds, input_bounds)
+ op_indices = (
+ enumerate(self.operands)
+ if index is None
+ else ([(index, self.operands[index])])
+ )
+ result = 0.0
+ for op_index, op in op_indices:
+ if op.propositional:
+ op_grounding_rows = None
+ else:
+ if groundings is None:
+ op_grounding_rows = op.grounding_table.values()
+ else:
+ op_grounding_rows = [None] * len(groundings)
+ for g_i, g in enumerate(groundings):
+ op_g = [
+ str(g.partial_grounding[slot])
+ for slot in self.operand_map[op_index]
+ ]
+ op_g = _Grounding(tuple(op_g) if len(op_g) > 1 else op_g[0])
+ op_grounding_rows[g_i] = op.grounding_table.get(op_g)
+ op_aggregate = op.neuron.aggregate_bounds(
+ op_grounding_rows, new_bounds[..., op_index]
+ )
+ if op_aggregate:
+ logging.info(
+ "↓ BOUNDS UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ if op.is_contradiction():
+ logging.info(
+ "↓ CONTRADICTION "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ result = result + op_aggregate
+ return result
+
+ def _logical_loss(
+ self, coeff: float = None, slacks: Union[bool, float] = None
+ ) -> torch.Tensor:
+ r"""Logical loss to create a loss on logical constraint violation.
+
+ Assumes a soft logic computation and calculates the loss on constraints
+ as defined in [equations 86-89](https://arxiv.org/pdf/2006.13155.pdf)
+ when slacks are given, the constraints are allowed to be violated
+ however this affects the neuron interpretability and should only be
+ used if the model is not strictly required to obey a classical
+ definition of logic
+
+ """
+ a = self.neuron.alpha
+ b = self.neuron.bias
+ w = self.neuron.weights
+ T, F = a, 1 - a
+ coeff = 1 if coeff is None else coeff
+ if isinstance(self, And):
+ TRUE = b - (w * (1 - T)).sum()
+ FALSE = b - (w * (1 - F))
+ true_hinge = torch.where(TRUE < T, T - TRUE, TRUE * 0)
+ false_hinge = torch.where(FALSE > F, FALSE - F, FALSE * 0)
+ if slacks:
+ if slacks is True:
+ slacks_false = false_hinge * (false_hinge > 0)
+ slacks_true = true_hinge * (true_hinge > 0)
+ false_hinge -= slacks_false
+ true_hinge -= slacks_true
+ self.neuron.slacks = (
+ slacks_true.detach().clone(),
+ slacks_false.detach().clone(),
+ )
+ else:
+ false_hinge -= slacks
+ self.neuron.feasibility = (
+ true_hinge.detach().clone(),
+ false_hinge.detach().clone(),
+ )
+
+ elif isinstance(self, Or):
+ TRUE = 1 - b + (w * T)
+ FALSE = 1 - b + (w * F).sum()
+ true_hinge = torch.where(TRUE < T, T - TRUE, TRUE * 0).sum()
+ false_hinge = torch.where(FALSE > F, FALSE - F, FALSE * 0)
+ elif isinstance(self, Implies):
+ TRUE = 1 - b + (w * T) # T = 1-F for x and T for y
+ FALSE = 1 - b + (w[0] * (1 - T)) + (w[1] * F)
+ true_hinge = torch.where(TRUE < T, T - TRUE, TRUE * 0).sum()
+ false_hinge = torch.where(FALSE > F, FALSE - F, FALSE * 0)
+ result = (true_hinge.square() + false_hinge.square()).sum()
+ return coeff * result
+
+ def neural_equivalence(self, other):
+ if (
+ isinstance(self.neuron, other.neuron)
+ and self.neuron.bias == other.neuron.bias
+ and len(self.neuron.weights) == len(other.neuron.weights)
+ and all(
+ self.neuron.weights[idx] == other.neuron.weights[idx]
+ for idx in range(len(self.neuron.weights))
+ )
+ ):
+ return True
+ return False
+
+
+class _NAryNeuron(_ConnectiveNeuron):
+ r"""N-ary connective neuron."""
+
+ def __init__(self, *formula, **kwds):
+ super().__init__(*formula, arity=len(formula), **kwds)
+
+
+class _BinaryNeuron(_ConnectiveNeuron):
+ r"""Restrict neurons to 2 inputs."""
+
+ def __init__(self, *formula, **kwds):
+ if len(formula) != 2:
+ raise Exception(
+ "Binary neurons expect 2 formulae as inputs, received "
+ f"{len(formula)}"
+ )
+ super().__init__(*formula, arity=2, **kwds)
+
+
+class _UnaryOperator(_ConnectiveFormula):
+ r"""Restrict operators to 1 input."""
+
+ def __init__(self, *formula: Formula, **kwds):
+ if len(formula) != 1:
+ raise Exception(
+ "Unary operator expect 1 formula as input, received " f"{len(formula)}"
+ )
+ super().__init__(*formula, arity=1, **kwds)
+
+
+class _Quantifier(_UnaryOperator):
+ r"""Symbolic container for quantifiers.
+
+ Parameters
+ ------------
+ kwds : dict
+ fully_grounded : bool
+ specifies if a full upward inference can be done on a
+ quantifier due to all the groundings being present inside it.
+ This applies to the lower bound of a `ForAll` and upper bound
+ of an `Exists`
+
+ Attributes
+ ----------
+ fully_grounded : bool
+ unique_var_slots : tuple of int
+ returns the slot index of each unique variable
+
+ """
+
+ def __init__(self, quantified_variable: "Variable", formula: Formula, **kwds):
+ self.quantified_variable = quantified_variable
+ super().__init__(formula, **kwds)
+ self.fully_grounded = kwds.get("fully_grounded", False)
+ self._grounding_set = set()
+ self._set_activation(**kwds)
+
+ @property
+ def expanded_unique_vars(self):
+ result = list(self.unique_vars)
+ for idx, v in enumerate(self.variables):
+ result.append(v)
+ return tuple(result)
+
+ @staticmethod
+ def _unique_variables_overlap(
+ source: Tuple["Variable", ...], destination: Tuple["Variable", ...]
+ ) -> Tuple["Variable", ...]:
+ """combines all predicate variables into a unique tuple
+ the tuple is sorted by the order of appearance of variables in
+ the operands
+ """
+ result = list()
+ for dst_var in destination:
+ if dst_var not in source:
+ result.append(dst_var)
+ return tuple(result)
+
+ def upward(self, **kwds) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = self.neuron.aggregate_world(self.operands[0].world)
+ if result:
+ if self.propositional:
+ self.neuron.reset_world(self.world)
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ n_groundings = len(self._grounding_set)
+ input_bounds = self._upward_bounds(self.operands[0])
+ if input_bounds is None:
+ return 0.0
+ if len(self._grounding_set) > n_groundings:
+ self._set_activation(world=self.world)
+ result = self.neuron.aggregate_bounds(
+ None,
+ self.func(input_bounds.permute([1, 0])),
+ bound=(
+ (Bound.UPPER if isinstance(self, ForAll) else Bound.LOWER)
+ if not self.fully_grounded
+ else None
+ ),
+ )
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ if self.is_contradiction():
+ logging.info(
+ "↑ CONTRADICTION "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+ def _set_activation(self, **kwds):
+ """Updates the neural activation according to grounding dimension size
+
+ The computation of a quantifier is implemented via one of the weighed
+ neurons, And/Or for ForAll/Exists.
+ At present, weighted quantifiers have not been well studied and is
+ therefore turned off
+ However the dimension of computation is different, computing over the
+ groundings of the input formula instead of multiple formulae, since
+ there can only be one formula to quantify over.
+ The activation is therefore required to grow according to number of
+ groundings present in the formula, which can grow as groundings
+ propagate via inference.
+
+ """
+ operator = (
+ "And"
+ if isinstance(self, ForAll)
+ else ("Or" if isinstance(self, Exists) else None)
+ )
+ kwds.setdefault("arity", len(self._grounding_set))
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NeuralActivation()(
+ activation={"weights_learning": False}, **kwds
+ )
+ self.func = self.neuron.activation(operator, direction=Direction.UPWARD)
+
+ @staticmethod
+ def _has_free_variables(
+ variables: Tuple["Variable", ...], operand: Formula
+ ) -> bool:
+ r"""Returns True if the quantifier contains free variables."""
+ return len(set(variables)) != len({*operand.unique_vars})
+
+ @property
+ def true_groundings(
+ self,
+ ) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""Returns a set of groundings that are True."""
+ valid_groundings = [
+ g for g in self._grounding_set if self.operands[0].state(g) is Fact.TRUE
+ ]
+ return self._groundings(valid_groundings) if valid_groundings else set()
+
+ def _upward_bounds(self, operand: Formula) -> Union[torch.Tensor, None]:
+ r"""Set Quantifier grounding table and return operand tensor."""
+ operand_grounding_set = set(operand.grounding_table)
+ if len(operand_grounding_set) == 0:
+ return
+
+ self._grounding_set = set(
+ [
+ grounding
+ for grounding in operand_grounding_set
+ if _gm.is_grounding_in_bindings(self, 0, grounding)
+ ]
+ )
+ return operand.get_data(*self._grounding_set) if self._grounding_set else None
+
+ def _groundings(self, groundings=None) -> Set[Union[str, Tuple[str, ...]]]:
+ """Internal usage to extract groundings as _Grounding object"""
+ return set(map(_Grounding.eval, groundings)) if groundings else self.groundings
+
+ @property
+ def groundings(self) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""returns a set of groundings as str or tuple of str"""
+ return set(map(_Grounding.eval, self._grounding_set))
+
+ def add_data(self, facts: Union[Tuple[float, float], Fact, Set]):
+ super().add_data(facts)
+ self._set_activation(world=self.world)
+
+
+class _NAryOperator(_ConnectiveFormula):
+ r"""N-ary connective operator"""
+
+ def __init__(self, *formula, **kwds):
+ super().__init__(*formula, arity=len(formula), **kwds)
+
+
+class _Grounding(_utils.MultiInstance, _utils.UniqueNameAssumption):
+ r"""Propositionalises constants for first-order logic
+
+ Returns a container for a string or a tuple of strings.
+ Follows the unique name assumption so that given constant(s) return the
+ same object
+ Decomposes multiple constants (from the tuple) by storing each str as a
+ separate grounding object but returns only the compound container.
+ This decomposition is used in grounding management to ensure that all
+ partial strings also follow the unique name assumption by returning the
+ same container
+
+ Parameters
+ ------------
+ constants : str or tuple of str
+
+ Examples
+ --------
+ ```python
+ _Grounding('person1')
+ _Grounding(('person1', 'date1'))
+ ```
+
+ Attributes
+ ----------
+ name : str
+ conversion of 'constants' param to str form
+ grounding_arity : int
+ length of the 'constants' param
+ partial_grounding : tuple(_Grounding)
+ tuple of groundings for decomposition when constants given as tuple
+
+ """
+
+ def __init__(self, constants: Union[str, Tuple[str, ...]]):
+ super().__init__(constants)
+ self.name = str(constants)
+ if isinstance(constants, tuple):
+ self.grounding_arity = len(constants)
+ self.partial_grounding = tuple(
+ map(self._partial_grounding_from_str, constants)
+ )
+ else:
+ self.grounding_arity = 1
+ self.partial_grounding = (self,)
+
+ @classmethod
+ def _partial_grounding_from_str(cls, constant: str) -> "_Grounding":
+ r"""Returns partial Grounding given grounding str"""
+ return _Grounding.instances[constant]
+
+ @classmethod
+ def ground_by_groundings(cls, *grounding: "_Grounding"):
+ r"""Reduce a tuple of groundings to a single grounding"""
+ return (
+ grounding[0]
+ if len(grounding) == 1
+ else cls.__class__(tuple(str(g) for g in grounding))
+ )
+
+ def __len__(self) -> int:
+ r"""Returns the length of the grounding arity"""
+ return self.grounding_arity
+
+ def __str__(self) -> str:
+ r"""Returns the name of the grounding"""
+ return self.name
+
+ @staticmethod
+ def eval(grounding: "_Grounding") -> Union[str, Tuple[str, ...]]:
+ r"""Returns the original constant(s) in str or tuple of str form"""
+ return eval(grounding.name) if grounding.grounding_arity > 1 else grounding.name
+
+
+class _NodeActivation:
+ def __call__(self, **kwds):
+ return getattr(
+ importlib.import_module("lnn.neural.activations.node"),
+ "_NodeActivation",
+ )(**kwds)
+
+
+class _NeuralActivation:
+ r"""Switch class, to choose a method from the correct activation class"""
+
+ def __init__(self, type=None):
+ self.neuron_type = type if type else NeuralActivation.LukasiewiczTransparent
+ _exceptions.AssertNeuronActivationType(self.neuron_type)
+ self.module = importlib.import_module(
+ f"lnn.neural.methods.{self.neuron_type.name.lower()}"
+ )
+
+ def __call__(self, **kwds):
+ return getattr(self.module, self.neuron_type.name)(**kwds)
+
+
+##
+# Public Classes
+#
+# All classes below should be exposed via the public API
+# The formulas are ordered alphabetically according to the API docs in
+# https://ibm.github.io/LNN/lnn/LNN.html
+##
+
+
+[docs]class Predicate(_LeafFormula):
+ r"""Creates a container for a predicate
+
+ Stores a table of truths, with columns specified by the arity and rows
+ indexed by the grounding
+
+ Parameters
+ ----------
+ name : str
+ name of the predicate
+ arity : int, optional
+ If unspecified, assumes a unary predicate
+
+ Examples
+ --------
+ ```python
+ P1 = Predicate('P1')
+ P2 = Predicate('P2', arity=2)
+ ```
+
+ """
+
+ def __init__(self, name: str, arity: int = 1, **kwds):
+ if arity is None:
+ raise Exception(f"arity expected as int > 0, received {arity}")
+ super().__init__(name=name, arity=arity, propositional=False, **kwds)
+ self._update_variables(tuple(Variable(f"?{i}") for i in range(self.arity)))
+
+[docs] def add_data(self, facts: Union[dict, set]):
+ r"""Populate predicate with facts
+
+ Facts required in dict or set
+ - dict for grounding-based facts
+ - set for broadcasting facts across all groundings
+ requires a set of 1 item
+ dict keys for groundings and values as facts
+ tuple facts required in bounds form `(Lower, Upper)`
+
+ """
+ super().add_data(facts)
+
+ def __call__(self, *args, **kwds):
+ r"""A called first-order logic predicate
+
+ This correctly instantiates a predicate with variables - which is required when
+ using the predicate in a compound formula. Calling the predicate allows the LNN
+ to construct the inheritance tree from subformulae.
+
+ Examples
+ --------
+ ```python
+ P, Q = Predicates('P', 'Q')
+ x, y = Variables('x', 'y')
+ And(P(x), Q(y)) # calling both predicates
+ ```
+ Here the conjunction inherits its variables from all subformulae, treating it as
+ an ordered unique collection (list).
+ """
+ return super().__call__(*args, **kwds)
+
+
+[docs]def Predicates(*predicates: str, **kwds):
+ r"""Instantiates multiple predicates.
+
+ Examples
+ --------
+ ```python
+ P1, P2 = Predicates("P1", "P2", arity=2)
+ ```
+
+ """
+ return utils.return1([Predicate(p, **kwds) for p in predicates])
+
+
+[docs]class Proposition(_LeafFormula):
+ r"""Creates propositional containers
+
+ Stores and retrieves single truth bounds instead of tables as in FOL case
+
+ Parameters
+ ----------
+ name : str
+ name of the proposition
+
+ Examples
+ --------
+ ```python
+ P = Proposition('Person')
+ ```
+
+ """
+
+ def __init__(self, name: str, **kwds):
+ super().__init__(name=name, arity=1, propositional=True, **kwds)
+
+[docs] def add_data(self, fact: Fact):
+ """Populate proposition with facts
+
+ Facts required in bool, tuple or None
+ None fact assumes `Unknown`
+ tuple fact required in bounds form `(Lower, Upper)`
+
+ """
+ super().add_data(fact)
+
+
+[docs]def Propositions(*propositions: str, **kwds):
+ r"""Instantiates multiple propositions.
+
+ Examples
+ --------
+ ```python
+ P1, P2 = Propositions("P1", "P2")
+ ```
+
+ """
+ return utils.return1([Proposition(p, **kwds) for p in propositions])
+
+
+[docs]class Variable:
+ r"""Free variables to quantify first-order logic formulae
+
+ Parameters
+ ------------
+ name : str
+ name of the free variable
+ type : str, optional
+ constant of the type associated with the free variable
+
+ Examples
+ --------
+ ```python
+ x = Variable('x', 'person')
+ ```
+
+ """
+
+ def __init__(self, name: str, type: Optional[str] = None):
+ self.name = name
+ self.type = type
+
+ def __str__(self) -> str:
+ r"""Returns the name of the free variable"""
+ return self.name
+
+
+[docs]def Variables(*variables: str, **kwds) -> Union[Variable, Tuple[Variable, ...]]:
+ """Instantiates multiple variables.
+
+ Examples
+ --------
+ ```python
+ x, y = Variables("x", "y")
+ ```
+
+ """
+ return utils.return1([Variable(v, **kwds) for v in variables])
+
+
+[docs]class And(_NAryNeuron):
+ r"""Symbolic n-ary [conjunction](https://en.wikipedia.org/wiki/Logical_conjunction).
+
+ Returns a logical conjunction where inputs can be [propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ ``*formula`` : Formula
+ A variable length argument list that accepts any number of input formulae objects as arguments.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B, C = Propositions('A', 'B', 'C')
+ And(A, B, C)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A, C = Predicates('A', 'C')
+ B = Predicate('B', arity=2)
+ And(A(x), B(x, y), C(y)))
+ ```
+
+ """
+
+ def __init__(self, *formula: Formula, **kwds):
+ kwds.setdefault("activation", {})
+ self.operator_str = self.get_operator_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(*formula, **kwds)
+
+ @staticmethod
+ def get_operator_str(type: NeuralActivation) -> str:
+ return f"{type.name[0]}∧" if type else "∧"
+
+
+[docs]class Or(_NAryNeuron):
+ r"""Symbolic n-ary [disjunction](https://en.wikipedia.org/wiki/Logical_disjunction).
+
+ Returns a logical disjunction where inputs can be [propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ ``*formula`` : Formula
+ A variable length argument list that accepts any number of input formulae objects as arguments.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B, C = Propositions('A', 'B', 'C')
+ Or(A, B, C)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A, C = Predicates('A', 'C')
+ B = Predicate('B', arity=2)
+ Or(A(x), B(x, y), C(y)))
+ ```
+
+ """
+
+ def __init__(self, *formula, **kwds):
+ kwds.setdefault("activation", {})
+ self.operator_str = self.get_operator_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(*formula, **kwds)
+
+ @staticmethod
+ def get_operator_str(type: NeuralActivation) -> str:
+ return f"{type.name[0]}∨" if type else "∨"
+
+
+[docs]class Implies(_BinaryNeuron):
+ r"""Symbolic binary [implication](https://en.wikipedia.org/wiki/Logical_implication).
+
+ Returns a logical implication node where inputs can be [propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ lhs : Formula
+ The left-hand side formula of the binary inputs to the connective.
+ rhs : Formula
+ The right-hand side formula of the binary inputs to the connective.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B = Propositions('A', 'B')
+ Implies(A, B)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A')
+ B = Predicate('B', arity=2)
+ Implies(A(x), B(x, y)))
+ ```
+
+ """
+
+ def __init__(self, lhs: Formula, rhs: Formula, **kwds):
+ self.operator_str = "→"
+ kwds.setdefault("activation", {})
+ kwds["activation"].setdefault("bias_learning", True)
+ super().__init__(lhs, rhs, **kwds)
+ self.operator_str = self.get_operator_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(lhs, rhs, **kwds)
+
+ @staticmethod
+ def get_operator_str(type: NeuralActivation) -> str:
+ # if type is NeuralActivation.Product:
+ # return "|"
+ return f"{type.name[0]}→" if type else "→"
+
+
+[docs]class Not(_UnaryOperator):
+ r"""Symbolic Negation
+
+ Returns a logical negation where inputs can be propositional,
+ first-order logic predicates or other connectives.
+
+ Parameters
+ ------------
+ formula : Formula
+ accepts a unary input Formula
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A = Proposition('A')
+ Not(A)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A', arity=2)
+ Not(A(x, y)))
+ ```
+
+ """
+
+ def __init__(self, formula: Formula, **kwds):
+ self.operator_str = "¬"
+ super().__init__(formula, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+[docs] def upward(self, **kwds) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ self.neuron.aggregate_world(
+ tuple(
+ _utils.negate_bounds(torch.tensor(self.operands[0].world)).tolist()
+ )
+ )
+ else:
+ if self.propositional:
+ groundings = {None}
+ else:
+ groundings = tuple(self.operands[0]._groundings)
+ for g in groundings:
+ if g not in self.grounding_table:
+ self._add_groundings(g)
+ bounds = self.neuron.aggregate_bounds(
+ None, _utils.negate_bounds(self.operands[0].get_data(*groundings))
+ )
+ if self.is_contradiction():
+ logging.info(
+ "↑ CONTRADICTION "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return bounds
+
+[docs] def downward(self, **kwds) -> torch.Tensor:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ self.operands[0].neuron.aggregate_world(
+ tuple(_utils.negate_bounds(torch.tensor(self.world)).tolist())
+ )
+ else:
+ if self.propositional:
+ groundings = {None}
+ else:
+ groundings = tuple(self._groundings)
+ for g in groundings:
+ if g not in self.operands[0]._groundings:
+ self.operands[0]._add_groundings(g)
+ bounds = self.operands[0].neuron.aggregate_bounds(
+ None, _utils.negate_bounds(self.get_data(*groundings))
+ )
+ if self.operands[0].is_contradiction():
+ logging.info(
+ "↓ CONTRADICTION "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ return bounds
+
+
+[docs]class Equivalent(_BinaryNeuron):
+ r"""Symbolic Equivalence - a bidirectional binary implication or IFF (if and only if) node.
+
+ Returns a logical bidirectional equivalence node where inputs can be [propositions](LNN.html#lnn.Proposition),
+ `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ lhs : Formula
+ The left-hand side formula of the binary inputs to the connective.
+ rhs : Formula
+ The right-hand side formula of the binary inputs to the connective.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B = Propositions('A', 'B')
+ Equivalent(A, B)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A')
+ B = Predicate('B', arity=2)
+ Equivalent(A(x), B(x, y)))
+ ```
+
+ """
+
+ def __init__(self, lhs: Formula, rhs: Formula, **kwds):
+ self.operator_str = "∧"
+ self.Imp1, self.Imp2 = Implies(lhs, rhs, **kwds), Implies(rhs, lhs, **kwds)
+ super().__init__(self.Imp1, self.Imp2, **kwds)
+ self.func = self.neuron.activation("And", direction=Direction.UPWARD)
+ self.func_inv = self.neuron.activation("And", direction=Direction.DOWNWARD)
+
+[docs] def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ groundings : str or tuple of str
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ self.Imp1.upward(groundings, **kwds)
+ self.Imp2.upward(groundings, **kwds)
+ return super().upward(groundings, **kwds)
+
+[docs] def downward(
+ self,
+ index: int = None,
+ groundings: Set[Union[str, Tuple[str, ...]]] = None,
+ **kwds,
+ ) -> float:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ index : int, optional
+ restricts downward inference to an operand at the specified index. If unspecified, all operands are updated.
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ self.Imp1.downward(index, groundings, **kwds)
+ self.Imp2.downward(index, groundings, **kwds)
+ return super().downward(index, groundings, **kwds)
+
+
+[docs]class Exists(_Quantifier):
+ r"""Symbolic existential quantifier.
+
+ When working with belief bounds - existential operators restrict upward inference to only work with the given formula's lower bound. Downward inference behaves as usual.
+
+ Parameters
+ ----------
+ ``*variables`` : Variable
+ formula : Formula
+ The FOL formula to quantify over, may be a connective formula or a Predicate.
+
+
+ Examples
+ --------
+ No free variables, quantifies over all of the variables in the formula.
+ ```python
+ Some_1 = Exists(birthdate(p, d)))
+ Some_2 = Exists(p, d, birthdate(p, d)))
+ ```
+
+ Free variables, quantifies over a subset of variables in the formula.
+ ```python
+ Some = Exists(p, birthdate(p, d)))
+ ```
+
+ Warning
+ -------
+ Quantifier with free variables, not yet implemented. It is required that we quantify over all the variables given in the formula, either by specifying all the variables or but not specifying any variables - which is equivalent to quantifying over all variables.
+
+ """
+
+ def __init__(self, *args, **kwds):
+ self.operator_str = "∃"
+ super().__init__(*args, **kwds)
+
+
+[docs]class ForAll(_Quantifier):
+ r"""Symbolic universal quantifier.
+
+ When working with belief bounds - universal operators restrict upward inference to only work with the given formula's upper bound. Downward inference behaves as usual.
+
+ Parameters
+ ----------
+ ``*variables`` : Variable
+ formula : Formula
+ The FOL formula to quantify over, may be a connective formula or a Predicate.
+
+ Examples
+ --------
+ No free variables, quantifies over all of the variables in the formula.
+ ```python
+ All_1 = ForAll(birthdate(p, d)))
+ All_2 = ForAll(p, d, birthdate(p, d)))
+ ```
+
+ Free variables, quantifies over a subset of variables in the formula.
+ ```python
+ All = ForAll(p, birthdate(p, d)))
+ ```
+
+ Warning
+ -------
+ Quantifier with free variables, not yet implemented. It is required that we quantify over all the variables given in the formula, either by specifying all the variables or but not specifying any variables - which is equivalent to quantifying over all variables.
+
+ """
+
+ def __init__(self, *args, **kwds):
+ self.operator_str = "∀"
+ kwds.setdefault("world", World.AXIOM)
+ super().__init__(*args, **kwds)
+
+[docs] def downward(self, **kwds) -> Union[torch.Tensor, None]:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = self.operands[0].neuron.aggregate_world(self.world)
+ if result:
+ logging.info(
+ "↓ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ else:
+ if not self._grounding_set:
+ return
+ operand = self.operands[0]
+ current_bounds = self.get_data()
+ groundings = operand.grounding_table.keys()
+ result = operand.neuron.aggregate_bounds(
+ [operand.grounding_table.get(g) for g in groundings], current_bounds
+ )
+ if result:
+ logging.info(
+ "↓ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ if operand.is_contradiction():
+ logging.info(
+ "↓ CONTRADICTION "
+ f"FOR:'{operand.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{operand.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ return result
+
+
+[docs]class Congruent(_NAryOperator):
+ r"""Symbolic Congruency
+
+ This is used to define nodes that are symbolically equivalent to one another
+ (despite the possibility of neural differences)
+
+ """
+
+ def __init__(self, *formulae: Formula, **kwds):
+ self.operator_str = "≅"
+ super().__init__(*formulae, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+ def __contains__(self, item):
+ return True if item in self.congruent_nodes else False
+
+[docs] def add_data(self, facts: Union[Fact, Tuple, Set, Dict]):
+ """Should not be called by the user"""
+ raise AttributeError(
+ "Should not be called directly by the user, instead use "
+ "`congruent_node.upward()` to evaluate the facts from the operands"
+ )
+
+ def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ groundings : str or tuple of str
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ if kwds.get("lifted"):
+ operands_world = torch.stack(
+ [torch.tensor(op.world) for op in self.operands], dim=-1
+ )
+ result = self.neuron.aggregate_world(
+ tuple(
+ torch.stack(
+ [
+ operands_world[..., 0, :].max(),
+ operands_world[..., 1, :].min(),
+ ],
+ dim=-1,
+ ).tolist()
+ )
+ )
+ if result:
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ upward_bounds = _gm.upward_bounds(self, self.operands, groundings)
+ if upward_bounds is None: # contradiction arresting
+ return
+ input_bounds, groundings = upward_bounds
+ grounding_rows = (
+ None
+ if self.propositional
+ else (
+ self.grounding_table.values()
+ if groundings is None
+ else [self.grounding_table.get(g) for g in groundings]
+ )
+ )
+ input_bounds = torch.stack(
+ [
+ input_bounds[..., 0, :].max(-1)[0],
+ input_bounds[..., 1, :].max(-1)[0],
+ ],
+ dim=-1,
+ )
+ result = self.neuron.aggregate_bounds(grounding_rows, input_bounds)
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+[docs] def downward(
+ self,
+ index: int = None,
+ groundings: Set[Union[str, Tuple[str, ...]]] = None,
+ **kwds,
+ ) -> Union[torch.Tensor, None]:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ index : int, optional
+ restricts downward inference to an operand at the specified index. If unspecified, all operands are updated.
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ if kwds.get("lifted"):
+ result = 0
+ for op_idx, op in enumerate(self.operands):
+ op_aggregate = op.neuron.aggregate_world(self.world)
+ result += op_aggregate
+ if op_aggregate:
+ logging.info(
+ "↓ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ else:
+ downward_bounds = _gm.downward_bounds(self, self.operands, groundings)
+ if downward_bounds is None: # contradiction arresting
+ return
+ parent, _, groundings = downward_bounds
+ op_indices = (
+ enumerate(self.operands)
+ if index is None
+ else ([(index, self.operands[index])])
+ )
+ result = 0
+ for op_index, op in op_indices:
+ if op.propositional:
+ op_grounding_rows = None
+ else:
+ if groundings is None:
+ op_grounding_rows = op.grounding_table.values()
+ else:
+ op_grounding_rows = [None] * len(groundings)
+ for g_i, g in enumerate(groundings):
+ op_g = [
+ str(g.partial_grounding[slot])
+ for slot in self.operand_map[op_index]
+ ]
+ op_g = _Grounding(tuple(op_g) if len(op_g) > 1 else op_g[0])
+ op_grounding_rows[g_i] = op.grounding_table.get(op_g)
+ op_aggregate = op.neuron.aggregate_bounds(op_grounding_rows, parent)
+ if op_aggregate:
+ logging.info(
+ "↓ BOUNDS UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ result = result + op_aggregate
+ return result
+
+ def extract_congruency(self, *formulae):
+ for idx, formula in enumerate(formulae):
+ if self not in formula.congruent_nodes:
+ formula.congruent_nodes.append(self)
+
+ def set_congruency(self):
+ for formula in self.operands:
+ if self not in formula.congruent_nodes:
+ formula.congruent_nodes.append(self)
+
+ def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ if kwds.get("lifted"):
+ operands_world = torch.stack(
+ [torch.tensor(op.world) for op in self.operands], dim=-1
+ )
+ result = self.neuron.aggregate_world(
+ tuple(
+ torch.stack(
+ [
+ operands_world[..., 0, :].max(),
+ operands_world[..., 1, :].min(),
+ ],
+ dim=-1,
+ ).tolist()
+ )
+ )
+ if result:
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ upward_bounds = _gm.upward_bounds(self, self.operands, groundings)
+ if upward_bounds is None: # contradiction arresting
+ return
+ input_bounds, groundings = upward_bounds
+ grounding_rows = (
+ None
+ if self.propositional
+ else (
+ self.grounding_table.values()
+ if groundings is None
+ else [self.grounding_table.get(g) for g in groundings]
+ )
+ )
+ input_bounds = torch.stack(
+ [
+ input_bounds[..., 0, :].max(-1)[0],
+ input_bounds[..., 1, :].min(-1)[0],
+ ],
+ dim=-1,
+ )
+ result = self.neuron.aggregate_bounds(grounding_rows, input_bounds)
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+
+[docs]class Function:
+ r"""Creates functions in first-order logic formulae
+
+ Parameters
+ ------------
+ name : str
+ name of the function
+ term : Variable, str, Grounding, or tuple of their combination
+ function arguments
+
+ Examples
+ --------
+ ```python
+ plus_func = Function('plus', X, Y)
+ x, y, z = Variables('x', 'y', 'z')
+ ```
+ """
+
+ # Add output arity
+ def __init__(self, name: str = "", input_dim: int = 1):
+ self.name = name
+ # The arity is expected to be known at construction.
+ self.input_dim = input_dim
+
+ # Constants and functions seen so far for each dimension.
+ self.groundings = dict()
+
+ def __str__(self):
+ args = ""
+ for arg_pos in range(self.input_dim):
+ args += "dim_" + str(arg_pos) + ", "
+
+ return self.name + "(" + args[0:-2] + ")"
+
+ def __repr__(self):
+ return self.__str__()
+
+ def __call__(
+ self,
+ *args: Union[
+ _Grounding,
+ List[_Grounding],
+ str,
+ List[str],
+ "Variable",
+ List["Variable"],
+ List[Union[str, _Grounding, "Variable"]],
+ ],
+ ) -> Union[_Grounding, "Function"]:
+ r"""Calls a function with arguments.
+
+ Parameters
+ ------------
+ args : List of _Grounding and/or output of called Function
+
+ Examples
+ --------
+ ```python
+ y = plus_func(zero, one)
+ ```
+ """
+
+ # If no input provided, it must map all available groundings.
+ if len(args) != self.input_dim and len(args) != 0:
+ raise Exception(
+ f"expected {self.input_dim} arguments" f"Received {len(args)}"
+ )
+
+ if all(
+ [
+ True if (isinstance(g, str) or isinstance(g, _Grounding)) else False
+ for g in args
+ ]
+ ):
+ # Full grounding
+ ground_str = ""
+ grounding = []
+ for arg_pos, arg in enumerate(args):
+ ground_str += str(arg) + ", "
+ grounding.append(str(arg))
+
+ if len(grounding) > 1:
+ grounding = tuple(grounding)
+ else:
+ grounding = (grounding[0],)
+ ground_out = self.groundings.get(grounding)
+ if ground_out is None:
+ ground_out = _Grounding(self.name + "(" + ground_str[0:-2] + ")")
+ self.groundings[grounding] = ground_out
+
+ return str(ground_out)
+
+ if all([isinstance(g, Variable) for g in args]):
+ # All variables
+ return self
+
+ # If not all groundings or variables we have a binding.
+ bindings = {}
+ for arg_pos, arg in enumerate(args):
+ if isinstance(arg, tuple) or isinstance(arg, Function):
+ bindings[arg_pos] = arg
+ elif isinstance(arg, str) or isinstance(arg, _Grounding):
+ bindings[arg_pos] = [arg]
+ else:
+ if not isinstance(arg, Variable):
+ raise TypeError(
+ f"Expected str, _Grounding, Variable, "
+ f"tuple or Function. Got {type(arg)}"
+ )
+ return self, bindings
+
+
+[docs]def Functions(*functions: str, **kwds):
+ r"""Instantiates multiple functions.
+
+ Examples
+ --------
+ ```python
+ f1, f2 = Functions("f1", "f2", input_dim=2)
+ ```
+
+ """
+ return utils.return1([Function(f, **kwds) for f in functions])
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from typing import Union, Tuple, Set
+
+from .connective_neuron import _ConnectiveNeuron
+from .formula import Formula
+from ... import _utils
+from ...constants import Direction, NeuralActivation
+
+_utils.logger_setup()
+
+
+class _BinaryNeuron(_ConnectiveNeuron):
+ r"""Restrict neurons to 2 inputs."""
+
+ def __init__(self, *formula, **kwds):
+ if len(formula) != 2:
+ raise Exception(
+ "Binary neurons expect 2 formulae as inputs, received "
+ f"{len(formula)}"
+ )
+ super().__init__(*formula, arity=2, **kwds)
+
+
+[docs]class Implies(_BinaryNeuron):
+ r"""
+ Symbolic binary [implication](https://en.wikipedia.org/wiki/Logical_implication).
+
+ Returns a logical implication node where inputs can be [propositions](
+ LNN.html#lnn.Proposition), `called` first-order logic [predicates](
+ LNN.html#lnn.Predicate) or any other [connective formulae](
+ LNN.html#symbolic-structure). Propositional inputs yield a propositional node,
+ whereas if any input is a predicate it will cause the connective to increase its
+ dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ lhs : Formula
+ The left-hand side formula of the binary inputs to the connective.
+ rhs : Formula
+ The right-hand side formula of the binary inputs to the connective.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B = Propositions('A', 'B')
+ Implies(A, B)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A')
+ B = Predicate('B', arity=2)
+ Implies(A(x), B(x, y)))
+ ```
+
+ """
+
+ def __init__(self, lhs: Formula, rhs: Formula, **kwds):
+ self.connective_str = "→"
+ kwds.setdefault("activation", {})
+ kwds["activation"].setdefault("bias_learning", True)
+ super().__init__(lhs, rhs, **kwds)
+ self.connective_str = self.get_connective_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(lhs, rhs, **kwds)
+
+ @staticmethod
+ def get_connective_str(type: NeuralActivation) -> str:
+ # if type is NeuralActivation.Product:
+ # return "|"
+ return f"{type.name[0]}→" if type else "→"
+
+
+[docs]class Equivalent(_BinaryNeuron):
+ r"""Symbolic Equivalence - a bidirectional binary implication or IFF
+ (if and only if) node.
+
+ Returns a logical bidirectional equivalence node where inputs can be [
+ propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](
+ LNN.html#lnn.Predicate) or any other [connective formulae](
+ LNN.html#symbolic-structure). Propositional inputs yield a propositional node,
+ whereas if any input is a predicate it will cause the connective to increase its
+ dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ lhs : Formula
+ The left-hand side formula of the binary inputs to the connective.
+ rhs : Formula
+ The right-hand side formula of the binary inputs to the connective.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B = Propositions('A', 'B')
+ Equivalent(A, B)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A')
+ B = Predicate('B', arity=2)
+ Equivalent(A(x), B(x, y)))
+ ```
+
+ """
+
+ def __init__(self, lhs: Formula, rhs: Formula, **kwds):
+ self.connective_str = "∧"
+ self.Imp1, self.Imp2 = Implies(lhs, rhs, **kwds), Implies(rhs, lhs, **kwds)
+ super().__init__(self.Imp1, self.Imp2, **kwds)
+ self.func = self.neuron.activation("And", direction=Direction.UPWARD)
+ self.func_inv = self.neuron.activation("And", direction=Direction.DOWNWARD)
+
+[docs] def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ groundings : str or tuple of str
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ self.Imp1.upward(groundings, **kwds)
+ self.Imp2.upward(groundings, **kwds)
+ return super().upward(groundings, **kwds)
+
+[docs] def downward(
+ self,
+ index: int = None,
+ groundings: Set[Union[str, Tuple[str, ...]]] = None,
+ **kwds,
+ ) -> float:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ index : int, optional
+ restricts downward inference to an operand at the specified index. If unspecified, all operands are updated.
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ result = super().downward(index, groundings, **kwds)
+ self.Imp1.downward(index, groundings, **kwds)
+ self.Imp2.downward(index, groundings, **kwds)
+ return result
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+import logging
+import itertools
+import typing
+from typing import Optional, Union, Tuple, Iterator, Set, List, Dict
+
+from abc import ABC
+
+from .grounding import _Grounding
+from .variable import Variable
+from .function import Function
+from .. import _trace
+from .._bindings import get_bindings
+from ... import _utils, _exceptions, utils
+from ...constants import Fact, World, Join
+
+import copy
+import torch
+import numpy as np
+
+_utils.logger_setup()
+subclasses: typing.Dict[str, object] = {}
+
+
+def _isinstance(obj, class_str) -> bool:
+ """
+ Returns True if an object is an instance of a class give that class name as a
+ string, otherwise False. The check is performed using the subclasses dictionary.
+ To see what the subclasses dictionary is populated with, refer to the init file of
+ this module.
+ """
+ return isinstance(obj, subclasses[class_str])
+
+
+[docs]class Formula(ABC):
+ r"""Symbolic container for a generic formula."""
+
+ def __init__(
+ self, *formulae: "Formula", name: Optional[str] = "", arity: int = None, **kwds
+ ):
+
+ self.join: Join = kwds.get("join", Join.INNER)
+
+ # construct edge and operand list for each formula
+ self.edge_list = list()
+ self.operands: List[Formula] = list()
+
+ # formula arity
+ self.arity: int = arity
+
+ # inherit propositional, variables, and graphs
+ self.propositional: bool = kwds.get("propositional")
+ self.variables: Tuple[Variable, ...] = kwds.get("variables")
+ self._inherit_from_subformulae(*formulae)
+
+ # formula naming
+ if _isinstance(self, "_LeafFormula"):
+ self.structure: str = name
+ self.name: str = name
+ else:
+ self.structure: str = self._formula_structure(True)
+ self.name: str = (
+ name if name else self._formula_structure(True, lambda x: x.name)
+ )
+
+ # formula grounding table maps grounded objects to table rows
+ self.grounding_table = None if self.propositional else dict()
+
+ # placeholder for neural variables and functions
+ self.neuron = None
+ self.func = None
+ self.func_inv = None
+ self.formula_number = None
+ self.operands_by_number = list()
+ self.congruent_nodes = list()
+
+ ##
+ # External function definitions
+ ##
+
+ def add_facts(self, *args, **kwds):
+ raise NameError(f"`add_facts` is deprecated, use `add_data` instead")
+
+[docs] def add_data(
+ self,
+ data: Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ):
+ r"""Add data to the formula in the form of classical facts or belief bounds.
+
+ Data given is a Fact or belief bounds assumes a propositional formula.
+ Data given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ data : Fact, belief bounds or dict
+ For propositional formulae, truths is given as either Facts or belief bounds (a tuple of 2 floats). For first-order logic formula, inputs truths are given as a dict. It is keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P, Q = Propositions("P", "Q")
+ P.add_data(Fact.TRUE)
+ Q.add_data((.1, .4))
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ Person.add_data({
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ })
+
+ # FOL with arity > 2
+ BD = Predicate("Birthdate", 2)
+ BD.add_data({
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ })
+ ```
+
+ """
+ if self.propositional: # Propositional facts
+ _exceptions.AssertBounds(data)
+ self.neuron.add_data(data)
+
+ else: # FOL facts
+ if isinstance(data, dict): # facts given per grounding
+ # replace fact keys (str -> _Groundings)
+ groundings = tuple(data.keys())
+ for g in groundings:
+ data[self._ground(g)] = data.pop(g)
+
+ # add missing groundings to `grounding_table`
+ groundings = tuple(data.keys())
+ self._add_groundings(*groundings)
+
+ # set facts for all groundings
+ table_facts = {self.grounding_table[g]: data[g] for g in groundings}
+ else:
+ raise Exception(
+ "FOL facts should be from [dict, set], "
+ f'"{self}" received {type(data)}'
+ )
+ self.neuron.add_data(table_facts)
+
+[docs] def add_labels(
+ self,
+ labels: Union[
+ Union[Fact, Tuple[float, float]],
+ Dict[Union[str, Tuple[str, ...]], Union[Fact, Tuple[float, float]]],
+ ],
+ ):
+ r"""Store labels as data within the symbolic container.
+
+ Labels given is a Fact or belief bounds assumes a propositional formula.
+ Labels given in a dict assumes a first-order logic formula,
+ keyed by the grounding and a value given as a Fact or belief bounds.
+
+ Parameters
+ ----------
+ labels : Fact, belief bounds or dict
+ For propositional formulae, facts are given as either Facts or bounds on beliefs (a tuple of 2 floats). For first-order logic formula, inputs are given as a dict. It is keyed by the grounding (a str for unary formlae or tuple of strings of larger arities), with values also as Facts or bounds on beliefs.
+
+ Examples
+ --------
+ ```python
+ # propositional
+ P, Q = Propositions("P", "Q")
+ P.add_labels(Fact.TRUE)
+ Q.add_labels((.1, .4))
+ ```
+ ```python
+ # first-order logic
+ Person = Predicate("Person")
+ Person.add_labels({
+ "Barack Obama": Fact.TRUE,
+ "Bo": (.1, .4)
+ })
+
+ # FOL with arity > 2
+ BD = Predicate("Birthdate", 2)
+ BD.add_labels({
+ ("Barack Obama", "04 August 1961"): Fact.TRUE,
+ ("Bo", "09 October 2008"): (.6, .75)
+ })
+ ```
+
+ """
+ if self.propositional: # Propositional labels
+ _exceptions.AssertBounds(labels)
+ self.labels = _utils.fact_to_bounds(labels, self.propositional)
+
+ else: # FOL labels
+ if not hasattr(self, "labels"):
+ self.labels = dict()
+ if isinstance(labels, dict): # labels given per grounding
+ _labels = copy.copy(labels)
+ for g in tuple(_labels.keys()):
+ # set labels for groundings, replace str keys -> Groundings
+ self.labels[self._ground(g)] = _utils.fact_to_bounds(
+ _labels.pop(g), self.propositional
+ )
+ else:
+ raise Exception(
+ "FOL facts should be from [dict, set], "
+ f'"{self}" received {type(labels)}'
+ )
+
+
+
+ def get_facts(self, *args, **kwds):
+ raise NameError(f"`get_facts` is deprecated, use `get_data` instead")
+
+[docs] def get_data(
+ self, *groundings: Union[str, Tuple[str, ...], _Grounding]
+ ) -> torch.Tensor:
+ r"""Returns the current beliefs of the formula.
+
+ Uses the given groundings or the entire `groundind_table` to slice out the
+ current belief bounds from the `bounds_table`.
+
+ Parameters
+ -------
+ ``*groundings``: str or tuple of str
+ NB - if unspecified, defaults to returning all the facts for the given formula. If specified, the table will be ordered according to the input grounding order.
+
+ """
+ if self.propositional or len(groundings) == 0:
+ return self.neuron.get_data()
+ table_rows = list(self.grounding_table.get(self._ground(g)) for g in groundings)
+ if all(row is None for row in table_rows):
+ return torch.Tensor(self.world)
+ result = self.neuron.get_data(table_rows)
+ return result
+
+[docs] def get_labels(self, *groundings: str) -> torch.Tensor:
+ r"""Returns the stored labels from the symbolic container."""
+ if self.propositional or len(groundings) == 0:
+ return self.labels
+ result = torch.stack([self.labels.get(self._ground(g)) for g in groundings])
+ return result[0] if len(groundings) == 1 else result
+
+ @property
+ def groundings(self) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""Returns the groundings to the user as str or tuple of str."""
+ if self.grounding_table:
+ return set(map(_Grounding.eval, self.grounding_table.keys()))
+
+ return set()
+
+ @property
+ def is_classically_resolved(self):
+ r"""Checks if the query node is in a classical state besides `Fact.UNKNOWN`."""
+ if self.propositional and _utils.is_classical_proposition(
+ tuple(self.get_data().tolist())
+ ):
+ return True
+ return False
+
+[docs] def is_contradiction(
+ self, bounds: torch.Tensor = None, stacked=False
+ ) -> torch.BoolTensor:
+ r"""Check if there are any bounds in contradiction."""
+ return self.contradicting_bounds(bounds, stacked).any()
+
+[docs] def contradicting_bounds(
+ self, bounds: torch.Tensor = None, stacked=False
+ ) -> torch.BoolTensor:
+ r"""Check which bounds are in contradiction."""
+ if stacked:
+ tensor = torch.logical_or(
+ self.neuron.is_contradiction(bounds[..., 0]),
+ self.neuron.is_contradiction(bounds[..., 1]),
+ )
+ return tensor.type(torch.bool)
+
+ return self.neuron.is_contradiction(bounds)
+
+[docs] def contradicting_stacked_bounds(
+ self, bounds: torch.Tensor = None
+ ) -> torch.BoolTensor:
+ r"""Check if bounds are in contradiction."""
+
+[docs] def is_equal(self, other: "Formula") -> bool:
+ r"""Returns True if two nodes are symbolically equivalent.
+
+ Formulae can be symbolically equivalent yet neurally different, example:
+ ```python
+ f = And(A, B, activation={"type": NeuralActivation.Lukasiewicz})
+ g = And(A, B, activation={"type": NeuralActivation.Godel})
+ ```
+ The above will return `True`, since `f` is symbolically equivalent to `g`
+ despite different neural configurations.
+
+ """
+ if self is other:
+ return True
+ result = list()
+ for f in self.congruent_nodes:
+ if _isinstance(f, "Congruent"):
+ result += [
+ other.structure == operand.structure for operand in f.operands
+ ]
+ return any(result)
+
+ def is_unweighted(self) -> bool:
+ return all([self.neuron.bias == w for w in self.neuron.weights])
+
+ def negation_absorption(
+ self, store: bool = True
+ ) -> (List[int], Tuple[Tuple["Formula"]]):
+ n_negations = []
+ edge_replace = []
+ operands = []
+
+ def recurse(formula):
+ for operand in formula.operands:
+ if _isinstance(operand, "Not"):
+ recurse(operand)
+ root_idx = len(n_negations) - 1
+ n_negations[root_idx] += 1
+ condition = [True] * len(self.neuron.weights)
+ condition[root_idx] = bool(root_idx % 2)
+ if store:
+ self.neuron.update_weights_where(
+ condition, -self.neuron.weights
+ )
+ self.operands[root_idx] = self.operands[root_idx].operands[0]
+ edge_replace.append(
+ (self.edge_list[root_idx], (self, self.operands[root_idx]))
+ )
+ else:
+ n_negations.append(0)
+ operands.append(operand)
+
+ recurse(self)
+ if store:
+ if edge_replace:
+ logging.info(f"ABSORBED NEGATIONS INTO WEIGHTS FOR: '{self.name}'")
+ return edge_replace, n_negations
+ else:
+ return operands, edge_replace, n_negations
+
+ def named_parameters(self) -> Iterator[Tuple[str, torch.Tensor]]:
+ yield from self.neuron.named_parameters()
+
+ def parameters(self) -> Iterator[torch.Tensor]:
+ for name, param in self.neuron.named_parameters():
+ yield param
+
+ def params(
+ self, *params: str, detach: bool = False
+ ) -> Union[torch.Tensor, List[torch.Tensor]]:
+ result = list()
+ for param in params:
+ if param in dict(self.neuron.named_parameters()):
+ result.append(
+ getattr(self.neuron, param).clone().detach()
+ if detach
+ else getattr(self.neuron, param)
+ )
+ else:
+ raise ValueError(f"{self} has no attribute: {param}")
+ return result[0] if len(params) == 1 else result
+
+[docs] def print(
+ self,
+ header_len: int = 50,
+ roundoff: int = 5,
+ params: bool = False,
+ grads: bool = False,
+ numbering: bool = False,
+ ):
+ r"""Print the states of groundings in a formula.
+
+ ```
+ OPEN Proposition: A UNKNOWN (L, U)
+
+ CLOSED Proposition: B FALSE (L, U)
+
+ OPEN Predicate: P1 (x)
+ "const_1" TRUE (L, U)
+ "const_2" CONTRADICTION (L, U)
+ "const_3" FALSE (L, U)
+
+ OPEN Predicate: P2 (x, y)
+ ("const_1", "const_5") TRUE (L, U)
+ ("const_2", "const_6") CONTRADICTION (L, U)
+ ("const_3", "const_7") FALSE (L, U)
+
+ OPEN And: And_0 (x, y)
+ Bindings: P1 (x: "const_1"), P2 (x: 'const_2', y: ['const_3', ...])
+ ('const_1', 'const_3') TRUE (L, U)
+ ('const_2', 'const_3') CONTRADICTION (L, U)
+ ('const_1', 'const_7') FALSE (L, U)
+
+ TRUE ForAll: ForAll_0 (y) UNKNOWN (L, U)
+ ```
+
+ """
+
+ def state_wrapper(grounding: _Grounding):
+ return (
+ f"'{grounding}'" if grounding.grounding_arity == 1 else f"{grounding}"
+ )
+
+ def round_bounds(grounding=None):
+ return tuple(
+ [
+ round(r, roundoff)
+ for r in (
+ self.get_data(grounding)
+ if self.propositional
+ else self.get_data(grounding)[0]
+ ).tolist()
+ ]
+ )
+
+ header = (
+ f"{str(self.world_state(True))} "
+ f"{self.__class__.__name__}"
+ f": {self.name}"
+ )
+ if params:
+ params = dict()
+ for name, symbol in _utils.param_symbols.items():
+ if hasattr(self.neuron, name):
+ val = getattr(self.neuron, name)
+ params[symbol] = f"{np.around(val.tolist(), roundoff)}" + (
+ f" grads {np.around(val.grad.tolist(), roundoff)}"
+ if grads and val.grad is not None
+ else ""
+ )
+ params = "params " + ", ".join([f"{k}: {v}" for k, v in params.items()])
+ else:
+ params = ""
+ number = (
+ f"{self.formula_number} {self.operands_by_number}: "
+ if self.formula_number is not None and numbering
+ else ""
+ )
+
+ # print propositional node - single bounds
+ if self.propositional:
+ states = (
+ f"{header:<{header_len}} "
+ f"{self.state().name:>13} "
+ f"{round_bounds()}\n"
+ f"{params}"
+ )
+ print(f"{number}{states}")
+
+ # print FOL node - table of bounds
+ else:
+ facts = (
+ [""]
+ if self.grounding_table is None
+ else (
+ [
+ (
+ f"{state_wrapper(g):{header_len}} "
+ f"{self.state(g).name:>13} "
+ f"{round_bounds(g)}\n"
+ )
+ for g in self.grounding_table
+ ]
+ )
+ )
+ binder = list()
+ for op_idx, op in enumerate(self.operands):
+ if not self.propositional and self._has_bindings(op_idx):
+ for i in range(len(self.var_remap[op_idx])):
+ if None not in self.bindings[op_idx][i]:
+ binder.append(
+ f"{str(op)} "
+ "{"
+ f"{str(self.operand_map[op_idx][i])}: "
+ f"{list(map(str, self.bindings[op_idx][i]))}"
+ "}"
+ )
+ bind_str = ("\nBindings: " + ", ".join(binder)) if binder else ""
+ header = f"{header} {bind_str}"
+ params = f"\n{params}" if params else ""
+ header = f"{header}{params}"
+ result = f"{header}\n" + "".join(facts)
+ print(f"{number}{result}")
+
+ def project_params(self):
+ self.neuron.project_params()
+
+ def rename(self, name: str):
+ self.name = name
+
+ def reset_bounds(self):
+ self.neuron.reset_bounds()
+
+ def reset_world(self, world: World):
+ _exceptions.AssertBoundsLen(world)
+ self.world = world if isinstance(world, tuple) else world.value
+ self.neuron.reset_world(world)
+
+ def set_formula_number(self, idx) -> int:
+ self.formula_number = idx
+ for operand in self.operands:
+ if operand.formula_number is None:
+ idx = operand.set_formula_number(idx + 1)
+ self.operands_by_number.append(operand.formula_number)
+ return idx
+
+ def set_join(self, join: Join):
+ _exceptions.AssertJoin(join)
+ self.join = join
+
+[docs] def set_negative_weights(
+ self, is_negative: bool = True, store: bool = True
+ ) -> (List[int], Tuple[Tuple["Formula"]]):
+ """absorb `Not` into weights and allow negative computation"""
+ self.neuron.set_negative_weights(is_negative)
+ return self.negation_absorption(store=store)
+
+[docs] def set_propositional(self, propositional: bool):
+ r"""Set's the neuron's world parameter."""
+ self.propositional = propositional
+
+ @property
+ def shape(self) -> torch.Size:
+ return self.neuron.bounds_table.shape
+
+[docs] def state(
+ self,
+ groundings: Union[
+ str, Tuple[str, ...], List[str], List[Tuple[str, ...]]
+ ] = None,
+ to_bool: bool = False,
+ bounds: torch.Tensor = None,
+ ) -> Union[torch.Tensor, Dict[Union[str, Tuple[str, ...]], torch.Tensor]]:
+ r"""Returns the state of a single grounded fact.
+
+ if to_bool flag is True, will map classical Facts to bool:
+ i.e. {Fact.True: True, FALSE': False}
+ The rest of the node states will return as str
+
+ Notes
+ -----
+ see section [F.2](https://arxiv.org/abs/2006.13155) for more
+ information on node states
+
+ """
+ if self.propositional:
+ result = self.neuron.state()
+ else:
+ if bounds is None:
+ if groundings is None or isinstance(groundings, list):
+ result = {
+ str(g): self.state(g)
+ for g in (
+ self.grounding_table if groundings is None else groundings
+ )
+ }
+ return result
+ groundings = self._ground(groundings)
+ bounds = self.get_data(groundings)
+ if len(bounds) == 0:
+ raise LookupError(f"grounding {groundings} not found in {str(self)}")
+ result = self.neuron.state(bounds[None, :])[0]
+ result = _utils.node_state(result)
+ return utils.fact_to_bool(result) if to_bool else result
+
+ @property
+ def unique_var_map(self) -> Dict:
+ result = {u: i for i, u in enumerate(self.unique_vars)}
+ if _isinstance(self, "_Quantifier"):
+ for idx, v in enumerate(self.variables):
+ result[v] = idx + len(self.unique_vars)
+ return result
+
+ @property
+ def world(self) -> World:
+ r"""Proxy to get the neuron's world parameter."""
+ return self.neuron.world
+
+ @world.setter
+ def world(self, new_world: Union[Tuple, World]):
+ r"""Proxy to set the neuron's world parameter."""
+ self.neuron.world = new_world
+
+[docs] def world_state(self, name=False):
+ r"""Returns the state of the `world` variable."""
+ try:
+ w = World(self.world)
+ return w.name if name else w
+ except ValueError:
+ return self.world
+
+ def And(self, *formulae: "Formula", **kwds) -> "And":
+ return subclasses["And"](*self._formula_vars(self, *formulae), **kwds)
+
+ def Or(self, *formulae: "Formula", **kwds) -> "Or":
+ return subclasses["Or"](*self._formula_vars(self, *formulae), **kwds)
+
+ def Implies(self, formula: "Formula", **kwds) -> "Implies":
+ return subclasses["Implies"](*self._formula_vars(self, formula), **kwds)
+
+ def Not(self, **kwds) -> "Not":
+ return subclasses["Not"](*self._formula_vars(self), **kwds)
+
+ def Equivalent(self, formula: "Formula", **kwds) -> "Equivalent":
+ return subclasses["Equivalent"](*self._formula_vars(self, formula), **kwds)
+
+ def Exists(self, **kwds) -> "Exists":
+ return subclasses["Exists"](self.unique_vars, self, **kwds)
+
+ def ForAll(self, **kwds) -> "ForAll":
+ return subclasses["ForAll"](*self.unique_vars, self, **kwds)
+
+ ##
+ # Internal function definitions
+ ##
+
+ def __call__(
+ self,
+ *variables: Variable,
+ bind: Dict[Variable, Union[str, List[str]]] = None,
+ ) -> Tuple[
+ "Formula",
+ List[Variable],
+ Tuple[Variable, ...],
+ Tuple[Union[List[_Grounding], List[None]]],
+ ]:
+ r"""Variable remapping between operator and operand variables.
+
+ Examples
+ --------
+ FOL formulae that appear in connectives are callable:
+ Note `A`, `B` in the `And`
+ ```python
+ x = Variable('x')
+ model['A'] = Predicate('A')
+ model['B'] = Predicate('B')
+ model['AB'] = And(A(x), B(x))
+ ```
+
+ Returns
+ -------
+ Formula:
+ reference to the child object
+ variables:
+ tuple of child's Variables
+ var_remap:
+ tuple of parent-to-child remapping Variables
+ bindings:
+ tuple of parent-to-child groundings to bind inference to single groundings are _Grounding multiple groundings are list(_Grounding)
+
+ """
+ if len(variables) != self.num_unique_vars:
+ raise Exception(
+ f"please check if the FOL arity of {self} is correctly set "
+ "for the number of variables "
+ f"variables length ({len(variables)}) must be the same "
+ f"length as `num_unique_vars` ({self.num_unique_vars})"
+ )
+ bindings = list()
+ if bind is None:
+ bind = dict()
+
+ variable_objects = list()
+
+ for v in variables:
+ if isinstance(v, str):
+ bindings.append([self._ground(v, arity_match=False)])
+ continue
+ elif isinstance(v, Variable):
+ variable_objects.append(v)
+ else:
+ raise TypeError(f"expected variable, received {type(v)}")
+
+ if v in bind:
+ if isinstance(bind[v], str): # a single binding
+ bindings.append([self._ground(bind[v], arity_match=False)])
+ elif isinstance(bind[v], list): # multiple bindings
+ bindings.append(
+ [self._ground(g, arity_match=False) for g in bind[v]]
+ )
+ elif isinstance(bind[v], Function): # A single function
+ bindings.append([bind[v]])
+ elif isinstance(bind[v], tuple): # A bound function
+ bindings.append([bind[v]])
+ else:
+ raise TypeError(
+ f"bindings expected as str, "
+ f"Function or list of str or "
+ f"Function, received {type(bind[v])}"
+ )
+ else:
+ bindings.append([None])
+ return self, self.variables, tuple(variable_objects), bindings
+
+ def __str__(self) -> str:
+ return self.name
+
+ def _add_groundings(self, *groundings: _Grounding):
+ r"""Adds missing groundings to `grounding_table` for those not yet stored.
+
+ Examples
+ --------
+ ```python
+ # for formulae with arity == 1:
+ formula._add_groundings(_Grounding_1, _Grounding_2)
+ ```
+ ```python
+ # for formulae with arity > 1:
+ groundings = ((_Grounding_1, _Grounding_7),
+ (_Grounding_2, _Grounding_8))
+ formula._add_groundings(*groundings)
+ ```
+
+ Warning
+ -------
+ groundings must be given in grounded form: `self._ground(grounding)`
+
+ """
+ missing_groundings = {g for g in groundings if g not in self.grounding_table}
+ if len(missing_groundings) == 0:
+ self._has_new_groundings = False
+ return
+ self._has_new_groundings = True
+ table_rows = self.neuron.extend_groundings(len(missing_groundings))
+ self.grounding_table.update(
+ {g: table_rows[i] for i, g in enumerate(missing_groundings)}
+ )
+
+ def _formula_structure(self, as_int, get_str=lambda x: x.structure) -> str:
+ r"""Determine a name for input formula(e)."""
+
+ def subformula_structure(
+ subformula: Formula,
+ operator: str = None,
+ subformula_vars: Tuple = None,
+ root_var_remap: dict = None,
+ ) -> str:
+ if subformula_vars is None:
+ root_var_remap = dict(
+ (k, k)
+ for k in (
+ self.expanded_unique_vars
+ if _isinstance(self, "_Quantifier")
+ else self.unique_vars
+ )
+ )
+ else:
+ if _isinstance(subformula, "_Quantifier"):
+ for v in subformula.expanded_unique_vars:
+ if v not in root_var_remap:
+ root_var_remap[v] = v
+ if subformula_vars != subformula.unique_vars:
+ root_var_remap = dict(
+ (
+ (
+ subformula.unique_vars[i],
+ root_var_remap[subformula_vars[i]],
+ )
+ if subformula.unique_vars[i] != subformula_vars[i]
+ else (subformula_vars[i], subformula_vars[i])
+ for i in range(len(subformula_vars))
+ )
+ )
+ result = [
+ (
+ f"{f.name}("
+ + _utils.list_to_str(
+ [
+ root_var_remap[v]
+ if not as_int
+ else subformula.unique_var_map[root_var_remap[v]]
+ if _isinstance(subformula, "_Quantifier")
+ else self.unique_var_map[root_var_remap[v]]
+ for v in [
+ subformula.expanded_unique_vars[_]
+ if _isinstance(subformula, "_Quantifier")
+ else subformula.unique_vars[_]
+ for _ in subformula.operand_map[i]
+ ]
+ ]
+ if subformula.operand_map[i]
+ else []
+ )
+ + ")"
+ )
+ if _isinstance(f, "Predicate")
+ else f"{f.name}"
+ if _isinstance(f, "Proposition")
+ else f"{f.structure}"
+ if _isinstance(f, "_Quantifier")
+ else (
+ "("
+ + subformula_structure(
+ f, f.connective_str, subformula.var_remap[i], root_var_remap
+ )
+ + ")"
+ )
+ if _isinstance(f, "_ConnectiveNeuron")
+ else (
+ f"{f.connective_str}"
+ + subformula_structure(
+ f, None, subformula.var_remap[i], root_var_remap
+ )
+ )
+ if _isinstance(f, "Not")
+ else ""
+ for i, f in enumerate(subformula.operands)
+ ]
+ return f" {operator} ".join(result) if operator else "".join(result)
+
+ if _isinstance(self, "_Quantifier"):
+ quantified_idxs = _utils.list_to_str(
+ [self.unique_var_map[v] for v in self.variables], ","
+ )
+ return (
+ f"({self.connective_str}{quantified_idxs}, "
+ f"{subformula_structure(self)})"
+ )
+
+ elif _isinstance(self, "Not"):
+ return (
+ f"{self.connective_str}{get_str(self.operands[0])}"
+ if self.propositional
+ else f"{self.connective_str}{subformula_structure(self)}"
+ )
+ return (
+ (
+ "("
+ + f" {self.connective_str} ".join([get_str(f) for f in self.operands])
+ + ")"
+ )
+ if self.propositional
+ else f"({subformula_structure(self, self.connective_str)})"
+ )
+
+ @staticmethod
+ def _formula_vars(*formulae: "Formula") -> List[Union["Formula", Tuple]]:
+ r"""Returns a list of formulae as wither called (when predicates)
+ or uncalled as connectives.
+ """
+ variables = list(
+ Variable(f"?{i}") for i in range(max([f.arity for f in formulae]))
+ )
+ return [
+ f(*variables[: f.arity])
+ if (not f.propositional and _isinstance(f, "Predicate"))
+ else f
+ for f in formulae
+ ]
+
+ def _ground(
+ self,
+ grounding: Union[str, Tuple[str, ...], _Grounding],
+ arity_match: bool = True,
+ ) -> _Grounding:
+ r"""Returns a single grounded object given a grounding in str form.
+
+ If the grounding is already an internal "Grounding" object, it will simply be
+ returned to the user as is.
+
+ Examples
+ --------
+ ```python
+ # for arity == 1
+ self._ground('str_1')
+ ```
+ ```python
+ # for arity > 1
+ grounding = ('str_1', 'str_2', ...)
+ self._ground(grounding)
+ ```
+
+ Warning
+ -------
+ This function can only ground one object at a time due to tuple confusion
+ for multiple objects
+
+ """
+ if Formula._is_grounded(grounding):
+ return grounding
+ if isinstance(grounding, tuple):
+ if not all([type(g) in [str, None] for g in grounding]):
+ raise Exception(
+ "expected groundings as tuple of str for num_unique_vars "
+ f" > 1, received {type(grounding)} {grounding}"
+ )
+ if len(grounding) != self.num_unique_vars and arity_match:
+ raise Exception(
+ "expected grounding length to be of "
+ f"arity {self.num_unique_vars}, received {grounding}"
+ )
+ else:
+ if self.num_unique_vars != 1 and arity_match:
+ raise Exception(
+ f"{self} received str as grounding, expected grounding "
+ f"({grounding}) as a tuple of len {self.num_unique_vars}"
+ )
+ return _Grounding(grounding)
+
+ def _ground_functions(self):
+ r"""Grounds a "Function" if given bindings that are fully bound."""
+ tmp_bindings = [
+ tuple([get_bindings(g) for g in op]) if op else ([None],)
+ for op in self.bindings
+ ]
+
+ for op_id, op in enumerate(self.operands):
+
+ # If there are groundings and partial bindings we can still
+ # create new groundings by combining the partials from
+ # groundings and bindings. But we need the ability
+ # to extract partial groundings without the grounding string.
+ # bindings = [g for g in product(*tmp_bindings[op_id])]
+ # for g in op.groundings: # Tuple
+ # for binding in bindings:
+ # new_g = [g[b] if binding[b] is None else binding[b]
+ # for b in range(len(binding))]
+ # op._add_groundings(tuple(new_g))
+
+ if all([False if g[0] is None else True for g in tmp_bindings[op_id]]):
+ for g in itertools.product(*tmp_bindings[op_id]):
+ if len(g) == 1:
+ op._add_groundings(op._ground(g[0]))
+ else:
+ op._add_groundings(op._ground(g))
+
+ @property
+ def _groundings(self) -> Set[_Grounding]:
+ """Internal usage to extract groundings as _Grounding object"""
+ return set(self.grounding_table.keys())
+
+ def _has_bindings(self, slot: int = None) -> bool:
+ r"""Returns True if Formula has any bindings."""
+ if isinstance(slot, int):
+
+ return (
+ True
+ if self.bindings[slot]
+ and any(
+ [
+ self.bindings[slot][i][j]
+ for i in range(len(self.bindings[slot]))
+ for j in range(len(self.bindings[slot][i]))
+ ]
+ )
+ else False
+ )
+ return any([self._has_bindings(i) for i in range(len(self.bindings))])
+
+ def _inherit_from_subformulae(self, *subformula: Union["Formula", Tuple]):
+ r"""Builds the local context for a formula using subformulae.
+
+ provides manual variable remapping if given with variables:
+ i.e. Formula used as a function via `__call__`
+ alternatively inherits remapping from operands if formula is not called
+
+ """
+
+ # inheritance variables
+ subformulae = list()
+ _operand_vars: List[Union[Tuple[Variable, ...], None]] = [None] * self.arity
+ _var_remap: List[Union[Tuple[Variable, ...], None]] = [None] * self.arity
+ _bindings: List[Union[Tuple[_Grounding, ...], None]] = [None] * self.arity
+
+ for slot, f in enumerate(subformula):
+
+ # variable remapping from `called` operands:
+ #
+ # ```python
+ # P = Predicate("P", arity=2)
+ # Q = Predicate("P", arity=2)
+ # And(P(x, y), Q(y, z))
+ # ```
+ if isinstance(f, tuple):
+ subformulae.append(f[0])
+ _operand_vars[slot] = f[1]
+ _var_remap[slot] = f[2]
+ _bindings[slot] = f[3]
+
+ self.edge_list.append((self, f[0]))
+ self.operands.append(f[0])
+
+ # automatically inherit variable remapping from `uncalled` operands
+ # for higher level connective formulae:
+ #
+ # ```python
+ # Implies(And(...), Or(...))
+ # ```
+ else:
+ if not f.propositional:
+ _var_remap[slot] = f.unique_vars
+ _operand_vars[slot] = f.unique_vars
+ _bindings[slot] = [[None]] * len(f.unique_vars)
+ subformulae.append(f)
+
+ self.edge_list.append((self, f))
+ self.operands.append(f)
+ self.operands: Tuple[Formula] = tuple(self.operands)
+
+ # set class variables as read-only tuples
+ self.operand_vars: Tuple[Tuple[Variable, ...], ...] = tuple(_operand_vars)
+ self.var_remap: Tuple[Tuple[Variable, ...], ...] = tuple(_var_remap)
+ self.bindings: Tuple[Tuple[_Grounding, ...], ...] = tuple(_bindings)
+
+ # inherit propositional flag from children
+ if self.propositional is None:
+ if _isinstance(self, "_Quantifier"):
+ self.set_propositional(
+ not subclasses["_Quantifier"]._has_free_variables(
+ self.variables, self.operands[0]
+ )
+ )
+ else:
+ self.set_propositional(
+ False if any([not f.propositional for f in subformulae]) else True
+ )
+
+ # inherit variables from children
+ if _isinstance(self, "_Quantifier") or (
+ not self.propositional and not _isinstance(self, "_LeafFormula")
+ ):
+ remap = self.var_remap
+ if _isinstance(self, "_Quantifier") and hasattr(self, "variables"):
+ remap = (
+ subclasses["_Quantifier"]._unique_variables_overlap(
+ self.variables, self.var_remap[0]
+ ),
+ )
+ self._update_variables(*remap)
+ self._update_map()
+
+ # expand formula graph to include all subformulae
+ if subformulae:
+ self.edge_list.extend([edge for f in subformulae for edge in f.edge_list])
+
+ @staticmethod
+ def _is_grounded(groundings: Union[_Grounding, str, Tuple[str, ...]]) -> bool:
+ r"""Returns True if the grounding is given in internal "Grounded" form."""
+ return isinstance(groundings, _Grounding)
+
+ @staticmethod
+ def _unique_variables(*variables: Tuple[Variable, ...]) -> Tuple:
+ r"""Combines all predicate variables into a unique tuple
+ the tuple is sorted by the order of appearance of variables in
+ the operands.
+ """
+ result = list()
+ for op_vars in variables:
+ if op_vars:
+ for v in op_vars:
+ if v not in result:
+ result.append(v)
+ return tuple(result)
+
+ def _update_map(self) -> None:
+ r"""Update the 'operand_map' to map parent groundings to operand groundings."""
+ self.operand_map: List[Tuple] = [None] * len(self.operand_vars)
+ for op_idx in range(len(self.var_remap)):
+ if self.var_remap[op_idx]:
+ op_map = [
+ self.unique_vars.index(op_var)
+ if op_var in self.unique_vars
+ else self.variables.index(op_var) + len(self.unique_vars)
+ for op_var in self.var_remap[op_idx]
+ ]
+ self.operand_map[op_idx] = tuple(op_map)
+
+ def _update_variables(self, *variables: Tuple[Variable, ...]) -> None:
+ r"""
+ **Notes**
+
+ If the formula grounding_arity is not specified, it will be inherited
+ from the variables. If variables are not specified, both the
+ `grounding_arity` and variables are inherited from groundings
+
+ """
+
+ self.unique_vars = Formula._unique_variables(*variables)
+ self.num_unique_vars = len(self.unique_vars)
+
+ def _contradiction_loss(self, coeff: float = None) -> torch.Tensor:
+ r"""Contradiction loss."""
+ if coeff is None:
+ coeff = 1
+ bounds = self.get_data()
+ x = bounds[..., 0] - bounds[..., 1]
+ return (self.is_contradiction() * coeff * x).sum()
+
+ def _uncertainty_loss(self, coeff: float = None) -> torch.Tensor:
+ r"""Uncertainty loss."""
+ if coeff is None:
+ coeff = 0
+ bounds = self.get_data()
+ x = bounds[..., 1] - bounds[..., 0]
+ return (self.is_contradiction().logical_not() * coeff * x).sum()
+
+ def _supervised_loss(self, coeff: float = None) -> Union[None, torch.Tensor]:
+ r"""Supervised loss."""
+ if coeff is None:
+ coeff = 1
+ loss = torch.nn.MSELoss()
+ if (
+ not hasattr(self, "labels")
+ or (self.propositional and not self.labels.numel())
+ or (not self.propositional and not self.labels)
+ ):
+ return
+ labels = self.get_labels()
+ if self.propositional:
+ return coeff * loss(self.get_data(), labels)
+ groundings = [g for g in labels if g in self.grounding_table]
+ if len(groundings) == 0:
+ return
+ return coeff * loss(self.get_data(*groundings), self.get_labels(*groundings))
+
+ increment_param_history = _trace.increment_param_history
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from typing import Union, List
+
+from .variable import Variable
+from .grounding import _Grounding
+from ... import _utils
+
+_utils.logger_setup()
+
+
+[docs]class Function:
+ r"""Creates functions in first-order logic formulae
+
+ Parameters
+ ------------
+ name : str
+ name of the function
+ term : Variable, str, Grounding, or tuple of their combination
+ function arguments
+
+ Examples
+ --------
+ ```python
+ plus_func = Function('plus', X, Y)
+ x, y, z = Variables('x', 'y', 'z')
+ ```
+ """
+
+ # Add output arity
+ def __init__(self, name: str = "", input_dim: int = 1):
+ self.name = name
+ # The arity is expected to be known at construction.
+ self.input_dim = input_dim
+
+ # Constants and functions seen so far for each dimension.
+ self.groundings = dict()
+
+ def __str__(self):
+ args = ""
+ for arg_pos in range(self.input_dim):
+ args += "dim_" + str(arg_pos) + ", "
+
+ return self.name + "(" + args[0:-2] + ")"
+
+ def __repr__(self):
+ return self.__str__()
+
+ def __call__(
+ self,
+ *args: Union[
+ _Grounding,
+ List[_Grounding],
+ str,
+ List[str],
+ Variable,
+ List[Variable],
+ List[Union[str, _Grounding, Variable]],
+ ],
+ ) -> Union[_Grounding, "Function"]:
+ r"""Calls a function with arguments.
+
+ Parameters
+ ------------
+ args : List of _Grounding and/or output of called Function
+
+ Examples
+ --------
+ ```python
+ y = plus_func(zero, one)
+ ```
+ """
+
+ # If no input provided, it must map all available groundings.
+ if len(args) != self.input_dim and len(args) != 0:
+ raise Exception(
+ f"expected {self.input_dim} arguments" f"Received {len(args)}"
+ )
+
+ if all(
+ [
+ True if (isinstance(g, str) or isinstance(g, _Grounding)) else False
+ for g in args
+ ]
+ ):
+ # Full grounding
+ ground_str = ""
+ grounding = []
+ for arg_pos, arg in enumerate(args):
+ ground_str += str(arg) + ", "
+ grounding.append(str(arg))
+
+ if len(grounding) > 1:
+ grounding = tuple(grounding)
+ else:
+ grounding = (grounding[0],)
+ ground_out = self.groundings.get(grounding)
+ if ground_out is None:
+ ground_out = _Grounding(self.name + "(" + ground_str[0:-2] + ")")
+ self.groundings[grounding] = ground_out
+
+ return str(ground_out)
+
+ if all([isinstance(g, Variable) for g in args]):
+ # All variables
+ return self
+
+ # If not all groundings or variables we have a binding.
+ bindings = {}
+ for arg_pos, arg in enumerate(args):
+ if isinstance(arg, tuple) or isinstance(arg, Function):
+ bindings[arg_pos] = arg
+ elif isinstance(arg, str) or isinstance(arg, _Grounding):
+ bindings[arg_pos] = [arg]
+ else:
+ if not isinstance(arg, Variable):
+ raise TypeError(
+ f"Expected str, _Grounding, Variable, "
+ f"tuple or Function. Got {type(arg)}"
+ )
+ return self, bindings
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from typing import Union
+
+from .formula import Formula
+from .node_activation import _NodeActivation
+from .variable import Variable
+from ... import _utils, utils
+from ...constants import Fact
+
+_utils.logger_setup()
+
+
+class _LeafFormula(Formula):
+ r"""Specifies activation functionality as nodes instead of neurons.
+
+ Assumes that all leaf formulae are propositions or predicates, therefore
+ uses the _NodeActivation accordingly
+
+ """
+
+ def __init__(self, *args, **kwds):
+ super().__init__(*args, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+
+[docs]class Predicate(_LeafFormula):
+ r"""Creates a container for a predicate
+
+ Stores a table of truths, with columns specified by the arity and rows
+ indexed by the grounding
+
+ Parameters
+ ----------
+ name : str
+ name of the predicate
+ arity : int, optional
+ If unspecified, assumes a unary predicate
+
+ Examples
+ --------
+ ```python
+ P1 = Predicate('P1')
+ P2 = Predicate('P2', arity=2)
+ ```
+
+ """
+
+ def __init__(self, name: str, arity: int = 1, **kwds):
+ if arity is None:
+ raise Exception(f"arity expected as int > 0, received {arity}")
+ super().__init__(name=name, arity=arity, propositional=False, **kwds)
+ self._update_variables(tuple(Variable(f"?{i}") for i in range(self.arity)))
+
+[docs] def add_data(self, facts: Union[dict, set]):
+ r"""Populate predicate with facts
+
+ Facts required in dict or set
+ - dict for grounding-based facts
+ - set for broadcasting facts across all groundings
+ requires a set of 1 item
+ dict keys for groundings and values as facts
+ tuple facts required in bounds form `(Lower, Upper)`
+
+ """
+ super().add_data(facts)
+
+ def __call__(self, *args, **kwds):
+ r"""A called first-order logic predicate
+
+ This correctly instantiates a predicate with variables - which is required when
+ using the predicate in a compound formula. Calling the predicate allows the LNN
+ to construct the inheritance tree from subformulae.
+
+ Examples
+ --------
+ ```python
+ P, Q = Predicates('P', 'Q')
+ x, y = Variables('x', 'y')
+ And(P(x), Q(y)) # calling both predicates
+ ```
+ Here the conjunction inherits its variables from all subformulae, treating it as
+ an ordered unique collection (list).
+ """
+ return super().__call__(*args, **kwds)
+
+
+[docs]def Predicates(*predicates: str, **kwds):
+ r"""Instantiates multiple predicates.
+
+ Examples
+ --------
+ ```python
+ P1, P2 = Predicates("P1", "P2", arity=2)
+ ```
+
+ """
+ return utils.return1([Predicate(p, **kwds) for p in predicates])
+
+
+[docs]class Proposition(_LeafFormula):
+ r"""Creates propositional containers
+
+ Stores and retrieves single truth bounds instead of tables as in FOL case
+
+ Parameters
+ ----------
+ name : str
+ name of the proposition
+
+ Examples
+ --------
+ ```python
+ P = Proposition('Person')
+ ```
+
+ """
+
+ def __init__(self, name: str, **kwds):
+ super().__init__(name=name, arity=1, propositional=True, **kwds)
+
+[docs] def add_data(self, fact: Fact):
+ """Populate proposition with facts
+
+ Facts required in bool, tuple or None
+ None fact assumes `Unknown`
+ tuple fact required in bounds form `(Lower, Upper)`
+
+ """
+ super().add_data(fact)
+
+
+[docs]def Propositions(*propositions: str, **kwds):
+ r"""Instantiates multiple propositions.
+
+ Examples
+ --------
+ ```python
+ P1, P2 = Propositions("P1", "P2")
+ ```
+
+ """
+ return utils.return1([Proposition(p, **kwds) for p in propositions])
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from .formula import Formula
+from .connective_neuron import _ConnectiveNeuron
+from ... import _utils
+from ...constants import NeuralActivation
+
+_utils.logger_setup()
+
+
+class _NAryNeuron(_ConnectiveNeuron):
+ r"""N-ary connective neuron."""
+
+ def __init__(self, *formula, **kwds):
+ super().__init__(*formula, arity=len(formula), **kwds)
+
+
+[docs]class And(_NAryNeuron):
+ r"""Symbolic n-ary [conjunction](https://en.wikipedia.org/wiki/Logical_conjunction).
+
+ Returns a logical conjunction where inputs can be [propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ ``*formula`` : Formula
+ A variable length argument list that accepts any number of input formulae objects as arguments.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B, C = Propositions('A', 'B', 'C')
+ And(A, B, C)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A, C = Predicates('A', 'C')
+ B = Predicate('B', arity=2)
+ And(A(x), B(x, y), C(y)))
+ ```
+
+ """
+
+ def __init__(self, *formula: Formula, **kwds):
+ kwds.setdefault("activation", {})
+ self.connective_str = self.get_connective_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(*formula, **kwds)
+
+ @staticmethod
+ def get_connective_str(type: NeuralActivation) -> str:
+ return f"{type.name[0]}∧" if type else "∧"
+
+
+[docs]class Or(_NAryNeuron):
+ r"""Symbolic n-ary [disjunction](https://en.wikipedia.org/wiki/Logical_disjunction).
+
+ Returns a logical disjunction where inputs can be [propositions](LNN.html#lnn.Proposition), `called` first-order logic [predicates](LNN.html#lnn.Predicate) or any other [connective formulae](LNN.html#symbolic-structure).
+ Propositional inputs yield a propositional node, whereas if any input is a predicate it will cause the connective to increase its dimension to also be a FOL node (i.e. stores a table of facts).
+
+ Parameters
+ ----------
+ ``*formula`` : Formula
+ A variable length argument list that accepts any number of input formulae objects as arguments.
+ name : str, optional
+ A custom name for the node to be used for identification and custom printing. If unspecified, defaults the structure of the node.
+ activation : dict, optional
+ Parameters given as a dictionary of configuration options, see the [neural configuration](../usage.html#neural-configuration) for more details
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A, B, C = Propositions('A', 'B', 'C')
+ Or(A, B, C)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A, C = Predicates('A', 'C')
+ B = Predicate('B', arity=2)
+ Or(A(x), B(x, y), C(y)))
+ ```
+
+ """
+
+ def __init__(self, *formula, **kwds):
+ kwds.setdefault("activation", {})
+ self.connective_str = self.get_connective_str(
+ kwds["activation"].get("type", None)
+ )
+ super().__init__(*formula, **kwds)
+
+ @staticmethod
+ def get_connective_str(type: NeuralActivation) -> str:
+ return f"{type.name[0]}∨" if type else "∨"
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+import logging
+from typing import Union, Tuple, Set, Dict
+
+import torch
+
+from .connective_formula import _ConnectiveFormula
+from .formula import Formula
+from .grounding import _Grounding
+from .node_activation import _NodeActivation
+from .. import _gm
+from ... import _utils
+from ...constants import Fact
+
+_utils.logger_setup()
+
+
+class _NAryOperator(_ConnectiveFormula):
+ r"""N-ary connective operator"""
+
+ def __init__(self, *formula, **kwds):
+ super().__init__(*formula, arity=len(formula), **kwds)
+
+
+[docs]class Congruent(_NAryOperator):
+ r"""Symbolic Congruency
+
+ This is used to define nodes that are symbolically equivalent to one another
+ (despite the possibility of neural differences)
+
+ """
+
+ def __init__(self, *formulae: Formula, **kwds):
+ self.connective_str = "≅"
+ super().__init__(*formulae, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+ def __contains__(self, item):
+ return True if item in self.congruent_nodes else False
+
+[docs] def add_data(self, facts: Union[Fact, Tuple, Set, Dict]):
+ """Should not be called by the user"""
+ raise AttributeError(
+ "Should not be called directly by the user, instead use "
+ "`congruent_node.upward()` to evaluate the facts from the operands"
+ )
+
+ def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ groundings : str or tuple of str
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ if kwds.get("lifted"):
+ operands_world = torch.stack(
+ [torch.tensor(op.world) for op in self.operands], dim=-1
+ )
+ result = self.neuron.aggregate_world(
+ tuple(
+ torch.stack(
+ [
+ operands_world[..., 0, :].max(),
+ operands_world[..., 1, :].min(),
+ ],
+ dim=-1,
+ ).tolist()
+ )
+ )
+ if result:
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ upward_bounds = _gm.upward_bounds(self, self.operands, groundings)
+ if upward_bounds is None: # contradiction arresting
+ return
+ input_bounds, groundings = upward_bounds
+ grounding_rows = (
+ None
+ if self.propositional
+ else (
+ self.grounding_table.values()
+ if groundings is None
+ else [self.grounding_table.get(g) for g in groundings]
+ )
+ )
+ input_bounds = torch.stack(
+ [
+ input_bounds[..., 0, :].max(-1)[0],
+ input_bounds[..., 1, :].max(-1)[0],
+ ],
+ dim=-1,
+ )
+ result = self.neuron.aggregate_bounds(grounding_rows, input_bounds)
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+[docs] def downward(
+ self,
+ index: int = None,
+ groundings: Set[Union[str, Tuple[str, ...]]] = None,
+ **kwds,
+ ) -> Union[torch.Tensor, None]:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ index : int, optional
+ restricts downward inference to an operand at the specified index. If unspecified, all operands are updated.
+ groundings : str or tuple of str, optional
+ restrict upward inference to a specific grounding or row in the truth table
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ if kwds.get("lifted"):
+ result = 0
+ for op_idx, op in enumerate(self.operands):
+ op_aggregate = op.neuron.aggregate_world(self.world)
+ result += op_aggregate
+ if op_aggregate:
+ logging.info(
+ "↓ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ else:
+ downward_bounds = _gm.downward_bounds(self, self.operands, groundings)
+ if downward_bounds is None: # contradiction arresting
+ return
+ parent, _, groundings = downward_bounds
+ op_indices = (
+ enumerate(self.operands)
+ if index is None
+ else ([(index, self.operands[index])])
+ )
+ result = 0
+ for op_index, op in op_indices:
+ if op.propositional:
+ op_grounding_rows = None
+ else:
+ if groundings is None:
+ op_grounding_rows = op.grounding_table.values()
+ else:
+ op_grounding_rows = [None] * len(groundings)
+ for g_i, g in enumerate(groundings):
+ op_g = [
+ str(g.partial_grounding[slot])
+ for slot in self.operand_map[op_index]
+ ]
+ op_g = _Grounding(tuple(op_g) if len(op_g) > 1 else op_g[0])
+ op_grounding_rows[g_i] = op.grounding_table.get(op_g)
+ op_aggregate = op.neuron.aggregate_bounds(op_grounding_rows, parent)
+ if op_aggregate:
+ logging.info(
+ "↓ BOUNDS UPDATED "
+ f"TIGHTENED:{op_aggregate} "
+ f"FOR:'{op.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{op.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ result = result + op_aggregate
+ return result
+
+ def extract_congruency(self, *formulae):
+ for idx, formula in enumerate(formulae):
+ if self not in formula.congruent_nodes:
+ formula.congruent_nodes.append(self)
+
+ def set_congruency(self):
+ for formula in self.operands:
+ if self not in formula.congruent_nodes:
+ formula.congruent_nodes.append(self)
+
+ def upward(
+ self, groundings: Set[Union[str, Tuple[str, ...]]] = None, **kwds
+ ) -> float:
+ if kwds.get("lifted"):
+ operands_world = torch.stack(
+ [torch.tensor(op.world) for op in self.operands], dim=-1
+ )
+ result = self.neuron.aggregate_world(
+ tuple(
+ torch.stack(
+ [
+ operands_world[..., 0, :].max(),
+ operands_world[..., 1, :].min(),
+ ],
+ dim=-1,
+ ).tolist()
+ )
+ )
+ if result:
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ upward_bounds = _gm.upward_bounds(self, self.operands, groundings)
+ if upward_bounds is None: # contradiction arresting
+ return
+ input_bounds, groundings = upward_bounds
+ grounding_rows = (
+ None
+ if self.propositional
+ else (
+ self.grounding_table.values()
+ if groundings is None
+ else [self.grounding_table.get(g) for g in groundings]
+ )
+ )
+ input_bounds = torch.stack(
+ [
+ input_bounds[..., 0, :].max(-1)[0],
+ input_bounds[..., 1, :].min(-1)[0],
+ ],
+ dim=-1,
+ )
+ result = self.neuron.aggregate_bounds(grounding_rows, input_bounds)
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+import logging
+from typing import Union, Tuple, Set
+
+import torch
+
+from .connective_formula import _ConnectiveFormula
+from .formula import Formula
+from .grounding import _Grounding
+from .neural_activation import _NeuralActivation
+from .node_activation import _NodeActivation
+from .variable import Variable
+from .. import _gm
+from ... import _utils
+from ...constants import Fact, World, Direction, Bound
+
+_utils.logger_setup()
+
+
+class _UnaryOperator(_ConnectiveFormula):
+ r"""Restrict operators to 1 input."""
+
+ def __init__(self, *formula: Formula, **kwds):
+ if len(formula) != 1:
+ raise Exception(
+ "Unary operator expect 1 formula as input, received " f"{len(formula)}"
+ )
+ super().__init__(*formula, arity=1, **kwds)
+
+
+class _Quantifier(_UnaryOperator):
+ r"""Symbolic container for quantifiers.
+
+ Parameters
+ ------------
+ kwds : dict
+ fully_grounded : bool
+ specifies if a full upward inference can be done on a
+ quantifier due to all the groundings being present inside it.
+ This applies to the lower bound of a `ForAll` and upper bound
+ of an `Exists`
+
+ Attributes
+ ----------
+ fully_grounded : bool
+ unique_var_slots : tuple of int
+ returns the slot index of each unique variable
+
+ """
+
+ def __init__(self, *args, **kwds):
+ variables = (
+ args[:-1]
+ if len(args) > 1
+ else args[-1][0].unique_vars
+ if isinstance(args[-1], tuple)
+ else args[-1].unique_vars
+ )
+ super().__init__(args[-1], variables=variables, **kwds)
+ self.fully_grounded = kwds.get("fully_grounded", False)
+ self._grounding_set = set()
+ self._set_activation(**kwds)
+
+ @property
+ def expanded_unique_vars(self):
+ result = list(self.unique_vars)
+ for idx, v in enumerate(self.variables):
+ result.append(v)
+ return tuple(result)
+
+ @staticmethod
+ def _unique_variables_overlap(
+ source: Tuple[Variable, ...], destination: Tuple[Variable, ...]
+ ) -> Tuple[Variable, ...]:
+ """combines all predicate variables into a unique tuple
+ the tuple is sorted by the order of appearance of variables in
+ the operands
+ """
+ result = list()
+ for dst_var in destination:
+ if dst_var not in source:
+ result.append(dst_var)
+ return tuple(result)
+
+ def upward(self, **kwds) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = self.neuron.aggregate_world(self.operands[0].world)
+ if result:
+ if self.propositional:
+ self.neuron.reset_world(self.world)
+ logging.info(
+ "↑ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ else:
+ n_groundings = len(self._grounding_set)
+ input_bounds = self._upward_bounds(self.operands[0])
+ if input_bounds is None:
+ return 0.0
+ if len(self._grounding_set) > n_groundings:
+ self._set_activation(world=self.world)
+ result = self.neuron.aggregate_bounds(
+ None,
+ self.func(input_bounds.permute([1, 0])),
+ bound=(
+ (Bound.UPPER if isinstance(self, ForAll) else Bound.LOWER)
+ if not self.fully_grounded
+ else None
+ ),
+ )
+ if result:
+ logging.info(
+ "↑ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ if self.is_contradiction():
+ logging.info(
+ "↑ CONTRADICTION "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return result
+
+ def _set_activation(self, **kwds):
+ """Updates the neural activation according to grounding dimension size
+
+ The computation of a quantifier is implemented via one of the weighed
+ neurons, And/Or for ForAll/Exists.
+ At present, weighted quantifiers have not been well studied and is
+ therefore turned off
+ However the dimension of computation is different, computing over the
+ groundings of the input formula instead of multiple formulae, since
+ there can only be one formula to quantify over.
+ The activation is therefore required to grow according to number of
+ groundings present in the formula, which can grow as groundings
+ propagate via inference.
+
+ """
+ operator = (
+ "And"
+ if isinstance(self, ForAll)
+ else ("Or" if isinstance(self, Exists) else None)
+ )
+ kwds.setdefault("arity", len(self._grounding_set))
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NeuralActivation()(
+ activation={"weights_learning": False}, **kwds
+ )
+ self.func = self.neuron.activation(operator, direction=Direction.UPWARD)
+
+ @staticmethod
+ def _has_free_variables(variables: Tuple[Variable, ...], operand: Formula) -> bool:
+ r"""Returns True if the quantifier contains free variables."""
+ return len(set(variables)) != len({*operand.unique_vars})
+
+ @property
+ def true_groundings(
+ self,
+ ) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""Returns a set of groundings that are True."""
+ return {
+ g
+ for g in self.operands[0].groundings
+ if self.operands[0].state(g) is Fact.TRUE
+ }
+
+ def _upward_bounds(self, operand: Formula) -> Union[torch.Tensor, None]:
+ r"""Set Quantifier grounding table and return operand tensor."""
+ operand_grounding_set = set(operand.grounding_table)
+ if len(operand_grounding_set) == 0:
+ return
+
+ self._grounding_set = set(
+ [
+ grounding
+ for grounding in operand_grounding_set
+ if _gm.is_grounding_in_bindings(self, 0, grounding)
+ ]
+ )
+ return operand.get_data(*self._grounding_set) if self._grounding_set else None
+
+ def _groundings(self, groundings=None) -> Set[Union[str, Tuple[str, ...]]]:
+ """Internal usage to extract groundings as _Grounding object"""
+ return set(map(_Grounding.eval, groundings)) if groundings else self.groundings
+
+ @property
+ def groundings(self) -> Set[Union[str, Tuple[str, ...]]]:
+ r"""returns a set of groundings as str or tuple of str"""
+ return set(map(_Grounding.eval, self._grounding_set))
+
+ def add_data(self, facts: Union[Tuple[float, float], Fact, Set]):
+ super().add_data(facts)
+ self._set_activation(world=self.world)
+
+
+[docs]class Not(_UnaryOperator):
+ r"""Symbolic Negation
+
+ Returns a logical negation where inputs can be propositional,
+ first-order logic predicates or other connectives.
+
+ Parameters
+ ------------
+ formula : Formula
+ accepts a unary input Formula
+
+ Examples
+ --------
+ ```python
+ # Propositional
+ A = Proposition('A')
+ Not(A)
+ ```
+ ```python
+ # First-order logic
+ x, y = Variables('x', 'y')
+ A = Predicate('A', arity=2)
+ Not(A(x, y)))
+ ```
+
+ """
+
+ def __init__(self, formula: Formula, **kwds):
+ self.connective_str = "¬"
+ super().__init__(formula, **kwds)
+ kwds.setdefault("propositional", self.propositional)
+ self.neuron = _NodeActivation()(**kwds.get("activation", {}), **kwds)
+
+[docs] def upward(self, **kwds) -> float:
+ r"""Upward inference from the operands to the operator.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ self.neuron.aggregate_world(
+ tuple(
+ _utils.negate_bounds(torch.tensor(self.operands[0].world)).tolist()
+ )
+ )
+ else:
+ if self.propositional:
+ groundings = {None}
+ else:
+ groundings = tuple(self.operands[0]._groundings)
+ for g in groundings:
+ if g not in self.grounding_table:
+ self._add_groundings(g)
+ bounds = self.neuron.aggregate_bounds(
+ None, _utils.negate_bounds(self.operands[0].get_data(*groundings))
+ )
+ if self.is_contradiction():
+ logging.info(
+ "↑ CONTRADICTION "
+ f"FOR:'{self.name}' "
+ f"FORMULA:{self.formula_number} "
+ )
+ return bounds
+
+[docs] def downward(self, **kwds) -> torch.Tensor:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ self.operands[0].neuron.aggregate_world(
+ tuple(_utils.negate_bounds(torch.tensor(self.world)).tolist())
+ )
+ else:
+ if self.propositional:
+ groundings = {None}
+ else:
+ groundings = tuple(self._groundings)
+ for g in groundings:
+ if g not in self.operands[0]._groundings:
+ self.operands[0]._add_groundings(g)
+ bounds = self.operands[0].neuron.aggregate_bounds(
+ None, _utils.negate_bounds(self.get_data(*groundings))
+ )
+ if self.operands[0].is_contradiction():
+ logging.info(
+ "↓ CONTRADICTION "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ return bounds
+
+
+[docs]class Exists(_Quantifier):
+ r"""Symbolic existential quantifier.
+
+ When working with belief bounds - existential operators restrict upward inference to only work with the given formula's lower bound. Downward inference behaves as usual.
+
+ Parameters
+ ----------
+ ``*variables`` : Variable
+ formula : Formula
+ The FOL formula to quantify over, may be a connective formula or a Predicate.
+
+
+ Examples
+ --------
+ No free variables, quantifies over all of the variables in the formula.
+ ```python
+ Some_1 = Exists(birthdate(p, d)))
+ Some_2 = Exists(p, d, birthdate(p, d)))
+ ```
+
+ Free variables, quantifies over a subset of variables in the formula.
+ ```python
+ Some = Exists(p, birthdate(p, d)))
+ ```
+
+ Warning
+ -------
+ Quantifier with free variables, not yet implemented. It is required that we quantify over all the variables given in the formula, either by specifying all the variables or but not specifying any variables - which is equivalent to quantifying over all variables.
+
+ """
+
+ def __init__(self, *args, **kwds):
+ self.connective_str = "∃"
+ super().__init__(*args, **kwds)
+
+
+[docs]class ForAll(_Quantifier):
+ r"""Symbolic universal quantifier.
+
+ When working with belief bounds - universal operators restrict upward inference to only work with the given formula's upper bound. Downward inference behaves as usual.
+
+ Parameters
+ ----------
+ ``*variables`` : Variable
+ formula : Formula
+ The FOL formula to quantify over, may be a connective formula or a Predicate.
+
+ Examples
+ --------
+ No free variables, quantifies over all of the variables in the formula.
+ ```python
+ All_1 = ForAll(birthdate(p, d)))
+ All_2 = ForAll(p, d, birthdate(p, d)))
+ ```
+
+ Free variables, quantifies over a subset of variables in the formula.
+ ```python
+ All = ForAll(p, birthdate(p, d)))
+ ```
+
+ Warning
+ -------
+ Quantifier with free variables, not yet implemented. It is required that we quantify over all the variables given in the formula, either by specifying all the variables or but not specifying any variables - which is equivalent to quantifying over all variables.
+
+ """
+
+ def __init__(self, *args, **kwds):
+ self.connective_str = "∀"
+ kwds.setdefault("world", World.AXIOM)
+ super().__init__(*args, **kwds)
+
+[docs] def downward(self, **kwds) -> Union[torch.Tensor, None]:
+ r"""Downward inference from the operator to the operands.
+
+ Parameters
+ ----------
+ lifted : bool, optional
+ flag that determines if lifting should be done on this node.
+
+ Returns
+ -------
+ tightened_bounds : float
+ The amount of bounds tightening or new information that is leaned by the inference step.
+
+ """
+ # Create (potentially) new groundings from functions
+ if not self.propositional:
+ self._ground_functions()
+
+ if kwds.get("lifted"):
+ result = self.operands[0].neuron.aggregate_world(self.world)
+ if result:
+ logging.info(
+ "↓ WORLD FREE-VARIABLE UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ else:
+ if not self._grounding_set:
+ return
+ operand = self.operands[0]
+ current_bounds = self.get_data()
+ groundings = operand.grounding_table.keys()
+ result = operand.neuron.aggregate_bounds(
+ [operand.grounding_table.get(g) for g in groundings], current_bounds
+ )
+ if result:
+ logging.info(
+ "↓ BOUNDS UPDATED "
+ f"TIGHTENED:{result} "
+ f"FOR:'{self.operands[0].name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{self.operands[0].formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ if operand.is_contradiction():
+ logging.info(
+ "↓ CONTRADICTION "
+ f"FOR:'{operand.name}' "
+ f"FROM:'{self.name}' "
+ f"FORMULA:{operand.formula_number} "
+ f"PARENT:{self.formula_number} "
+ )
+ return result
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from typing import Optional, Union, Tuple
+
+from ... import _utils, utils
+
+_utils.logger_setup()
+
+
+[docs]class Variable:
+ r"""Free variables to quantify first-order logic formulae
+
+ Parameters
+ ------------
+ name : str
+ name of the free variable
+ type : str, optional
+ constant of the type associated with the free variable
+
+ Examples
+ --------
+ ```python
+ x = Variable('x', 'person')
+ ```
+
+ """
+
+ def __init__(self, name: str, type: Optional[str] = None):
+ self.name = name
+ self.type = type
+
+ def __str__(self) -> str:
+ r"""Returns the name of the free variable"""
+ return self.name
+
+
+[docs]def Variables(*variables: str, **kwds) -> Union[Variable, Tuple[Variable, ...]]:
+ """Instantiates multiple variables.
+
+ Examples
+ --------
+ ```python
+ x, y = Variables("x", "y")
+ ```
+
+ """
+ return utils.return1([Variable(v, **kwds) for v in variables])
+
+
+##
+# Copyright 2022 IBM Corp. All Rights Reserved.
+#
+# SPDX-License-Identifier: Apache-2.0
+##
+
+# flake8: noqa: E501
+
+from typing import Union, Tuple, List, TypeVar, Iterable
+
+from . import _utils
+from .constants import Fact
+from lnn.symbolic.logic.leaf_formula import Predicate
+
+import re
+import random
+import itertools
+import numpy as np
+from tabulate import tabulate
+import matplotlib.pyplot as plt
+
+TRUE = Fact.TRUE
+FALSE = Fact.FALSE
+
+
+def split_string_into_groundings(state: str) -> Tuple[str]:
+ r"""
+
+ Parameters
+ ----------
+ :param state: The state is given as a string value representing the groundings; i.e "('T','T')"
+
+ Examples
+ --------
+ P,Q = Predicate("P","Q")
+ x,y = Variables("x","y")
+ PQ = Or(P(x), Q(y))
+ PQ.upward()
+ PQ.state(("T","T")) returns Fact.TRUE
+
+ Returns
+ -------
+ Groundings, given as strings, as a tuple of strings ; i.e "('T','T')" -> ("T","T")
+ """
+ pattern = r'[\'"()]'
+ grounding_strings = re.sub(pattern, "", state)
+ partial_groundings = grounding_strings.split(",")
+ partial_groundings = [pg.strip() for pg in partial_groundings]
+ return tuple(partial_groundings)
+
+
+def get_binary_truth_table(formulae: dict) -> dict:
+ r"""
+
+ Parameters
+ ----------
+ :param formulae: Formulae is a dictionary with str:formula format ;i.e {"P or Q": <lnn.symbolic.logic.n_ary_neuron >}
+
+ Returns
+ -------
+ Truth table in a dictionary format
+
+ """
+ table = dict()
+ groundings = set()
+ for f in formulae.values():
+ groundings.update(f.groundings)
+ groundings = alphanumeric_sort(groundings)
+ table[""] = [g for g in groundings]
+ for name, formula in formulae.items():
+ table[name] = [formula.state(g).name for g in groundings]
+ return table
+
+
+def alphanumeric_sort(iterable: Iterable):
+ def get_int(text):
+ return int(text) if text.isdigit() else text
+
+ def alphanum_key(key):
+ return [get_int(c) for c in re.split("([0-9]+)", key)]
+
+ return sorted(iterable, key=alphanum_key)
+
+
+def get_ternary_table(formulae: dict, unique_groundings: List[str] = None) -> dict:
+ keys = list(list(formulae.values())[0].state().keys())
+ formula = list(formulae.keys())[0]
+ keys = [split_string_into_groundings(key) for key in keys]
+ operator = list(formulae.values())[0]
+ if unique_groundings is None:
+ # unique_groundings = sorted(list(set(itertools.chain.from_iterable(keys))))
+ unique_groundings = ["F", "U", "T"]
+ grounding_map = dict(zip(range(len(unique_groundings)), unique_groundings))
+ number_of_unique_groundings = len(unique_groundings)
+ grounding_grid = np.zeros(
+ (number_of_unique_groundings, number_of_unique_groundings), dtype="int,int"
+ )
+ truth_grid = np.array(
+ [[""] * number_of_unique_groundings] * number_of_unique_groundings, dtype="<U10"
+ )
+ for i in range(grounding_grid.shape[0]):
+ for j in range(grounding_grid.shape[1]):
+ row, column = grounding_map[i], grounding_map[j]
+ truth_grid[i, j] = operator.state((row, column)).name
+ row_title = np.atleast_2d(unique_groundings).T
+ column_data = np.atleast_2d([formula] + unique_groundings)
+ truth_grid = np.hstack((row_title, truth_grid))
+ truth_grid = np.vstack((column_data, truth_grid))
+ return truth_grid
+
+
+def get_n_ary_truth_table(formulae: dict, unique_groundings: List[str] = None) -> dict:
+ r"""
+
+ Parameters
+ ----------
+ :param formulae: Formulae is a dictionary with str:formula format ;i.e {"P or Q": <lnn.symbolic.logic.n_ary_neuron >}
+ :param unique_groundings: Unique groundings that fill either the rows or columns i.e ["F", "U", "T"]
+
+ Returns
+ -------
+ Truth table in a dictionary format
+
+ """
+ keys = list(list(formulae.values())[0].state().keys())
+ formula = list(formulae.keys())[0]
+ keys = [split_string_into_groundings(key) for key in keys]
+ if unique_groundings is None:
+ unique_groundings = sorted(list(set(itertools.chain.from_iterable(keys))))
+ truth = {f"{formula}": unique_groundings}
+ for unique_grounding in unique_groundings:
+ table_columns = list(
+ filter(
+ lambda partial_grounding: partial_grounding[0].startswith(
+ f"{unique_grounding}"
+ ),
+ keys,
+ )
+ )
+ for _, formula in formulae.items():
+ truth[unique_grounding] = [
+ formula.state(table_column).name for table_column in table_columns
+ ]
+ return truth
+
+
+[docs]def pretty_truth_table(formulae: dict, unique_groundings: List[str] = None) -> None:
+ r"""
+
+ Parameters
+ ----------
+ :param formulae: Formulae is a dictionary with str:formula format ;i.e {"P or Q": <lnn.symbolic.logic.n_ary_neuron >}
+ :param arity: The number of variables specified
+ :param unique_groundings: unique_groundings: Unique groundings that fill either the rows or columns i.e ["F", "U", "T"]
+
+ Returns
+ -------
+ A pretty truth table
+ """
+ keys = list(list(formulae.values())[0].state().keys())
+ if len(keys[0]) <= 2:
+ table = get_binary_truth_table(formulae)
+ print(tabulate(table, headers="keys", tablefmt="fancy_grid"))
+ else:
+ table = get_ternary_table(formulae, unique_groundings)
+ print(tabulate(table, tablefmt="fancy_grid"))
+
+
+def generate_truth_table(P: Predicate, Q: Predicate, states=None) -> None:
+ r"""
+
+ Parameters
+ ----------
+ P: Predicate P
+ Q: Predicate Q
+ states: Data that you would like to each of the predicates
+
+ Returns
+ -------
+ Nothing, causes side effect on P and Q
+ """
+ if states is None:
+ states = [Fact.FALSE, Fact.UNKNOWN, Fact.TRUE]
+ idx = [f"{i}" for i in range(len(states))]
+ data = dict(zip(idx, states))
+ P.add_data(data)
+ Q.add_data(data)
+
+
+def truth_table(n: int, states=None) -> List[Tuple[Fact, ...]]:
+ if states is None:
+ states = [FALSE, TRUE]
+ return list(itertools.product(states, repeat=n))
+
+
+def truth_table_dict(*args: str, states=None):
+ if states is None:
+ states = [FALSE, TRUE]
+ for instance in itertools.product(states, repeat=len(args)):
+ yield dict(zip(args, instance))
+
+
+def fact_to_bool(*fact: Fact) -> Union[Fact, bool, Tuple[bool, ...]]:
+ if len(fact) > 1:
+ return tuple(map(fact_to_bool, fact))
+ if fact[0] is TRUE:
+ return True
+ elif fact[0] is FALSE:
+ return False
+ else:
+ return fact[0]
+
+
+def bool_to_fact(*truth: bool) -> Union[Fact, Tuple[Fact, ...]]:
+ if len(truth) > 1:
+ return tuple(map(bool_to_fact, truth))
+ return TRUE if truth[0] else FALSE
+
+
+[docs]def predicate_truth_table(*args: str, arity: int, model, states=None):
+ """
+ predicate_truth_table("p", "q", "r", model=model)
+
+ randomises the truth table into a predicate by str(int) rows
+
+ Returns
+ -------
+ model : Model
+ """
+ if states is None:
+ states = [FALSE, TRUE]
+ from lnn import Predicate # noqa: F401
+
+ n = len(args)
+ TT = np.array(truth_table(n, states))
+ _range = list(range(len(TT)))
+ for idx, arg in enumerate(args):
+ model[arg] = Predicate(arg, arity=arity)
+ random.shuffle(_range)
+ for i in _range:
+ grounding = f"{i}" if arity == 1 else (f"{i}",) * arity
+ truth = TT[i, idx].item()
+ model[arg].add_data({grounding: truth})
+ return model
+
+
+def plot_loss(total_loss, losses):
+ loss, cummulative_loss = total_loss
+ fig, axs = plt.subplots(1, 2)
+ fig.suptitle("Model Loss")
+ axs[0].plot(np.array(loss))
+ for ax in axs.flat:
+ ax.set(xlabel="Epochs", ylabel="Loss")
+ axs[0].legend(["Total Loss"])
+ axs[1].plot(np.array(cummulative_loss))
+ axs[1].legend([loss.value.capitalize() for loss in losses])
+ plt.show()
+
+
+Model = TypeVar("Model")
+
+
+def plot_params(self: Model):
+ legend = []
+ for node in self.nodes.values():
+ if hasattr(node, "parameter_history"):
+ for param, data in node.parameter_history.items():
+ if isinstance(data[0], list):
+ operands = list(node.operands)
+ legend_idxs = [f"_{operands[i]}" for i in list(range(len(data[0])))]
+ else:
+ legend_idxs = [""]
+ [
+ legend.append(f"{node.name} {_utils.param_symbols[param]}{i}")
+ for i in legend_idxs
+ ]
+ plt.plot(data)
+ plt.xlabel("Epochs")
+ plt.legend(legend)
+ plt.title(f"{self.name} Parameters")
+ plt.show()
+
+
+def return1(args: Union[List, Tuple]):
+ if len(args) == 1:
+ return args[0]
+ return args
+
+