Bridging Logic and Python
Write logical axioms using familiar Python constructs
Benefit from mypy validation and catch errors early
Integration with datalog engines, answer-set programming, theorem provers, OWL-DL, and Probablistic Logic
from pydantic import BaseModel
from typedlogic import FactMixin, Term
from typedlogic.decorators import axiom
ID = str
class Link(BaseModel, FactMixin):
"""A link between two entities"""
source: ID
target: ID
class Path(BaseModel, FactMixin):
"""An N-hop path between two entities"""
source: ID
target: ID
hops: int
@axiom
def path_from_link(x: ID, y: ID):
"""If there is a link from x to y, there is a path from x to y"""
assert Link(source=x, target=y) >> Path(source=x, target=y, hops=1)
@axiom
def transitivity(x: ID, y: ID, z: ID, d1: int, d2: int):
"""Transitivity of paths, plus hop counting"""
assert ((Path(source=x, target=y, hops=d1) & Path(source=y, target=z, hops=d2)) >>
Path(source=x, target=z, hops=d1+d2))from typedlogic.integrations.souffle_solver import SouffleSolver
from links import Link
import links as links
solver = SouffleSolver()
solver.load(links) ## source for definitions and axioms
# Add data
links = [Link(source='CA', target='OR'), Link(source='OR', target='WA')]
for link in links:
solver.add(link)
model = solver.model()
for fact in model.iter_retrieve("Path"):
print(fact)Path(source='CA', target='OR', hops=1)
Path(source='OR', target='WA', hops=1)
Path(source='CA', target='WA', hops=2)∀[x:ID y:ID]. Link(x, y) → Path(x, y, 1)
∀[x:ID y:ID z:ID d1:int d2:int]. Path(x, y, d1) ∧ Path(y, z, d2) → Path(x, z, d1+d2)