from typedlogic.registry import get_solver

py-typedlogic：为您的数据模型提供Pythonic逻辑。

直接在Python中定义逻辑谓词，如Pydantic、dataclasses、SQLModel或纯Python对象

# links.py
from pydantic import BaseModel
from typedlogic import FactMixin, Term

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, consisting of one or more links"""
    source: ID
    target: ID
    hops: int

此数据模型有两个类，Link和Path。这些也对应于逻辑理论中的谓词签名。

您可以使用它创建对象（逻辑术语中的 grounding terms）使用正常的Python代码

links = []
for source, target in [('CA', 'OR'), ('OR', 'WA')]:
   links.append(link)

使用Python语法定义逻辑约束或规则

from typedlogic.decorators import axiom

@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"""
    if Link(source=x, target=y):
        assert 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"""
    if Path(source=x, target=y, hops=d1) and Path(source=y, target=z, hops=d2):
        assert Path(source=x, target=z, hops=d1+d2)

使用求解器推断新事实

from typedlogic.registry import get_solver
from links import Link

solver = get_solver("clingo")
solver.load(links) 
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)

prints

Path(source='CA', target='OR')
Path(source='OR', target='WA')
Path(source='CA', target='WA')

关键特性

• 使用Python语法编写逻辑公理和规则（但也可以独立使用此功能）
• 受益于强类型和mypy验证
• 与多个一阶逻辑求解器和逻辑编程引擎集成
• 在FOL、规则和逻辑模型的多种语法之间进行互转换
• 与OWL-DL集成
• 与Python库如Pydantic集成
• 命令行和Python接口

安装

使用pip安装TypedLogic

pip install "typedlogic"

下一步

• 查阅主文档