Logical Unification

0.4.7 · active · verified Sat Apr 11

Logical Unification is a Python library that provides capabilities for logical unification, a core concept in logic programming and automated reasoning. It enables solving equations between symbolic expressions by finding substitutions for variables. The library is a fork of the original 'unification' project, designed with a generator-based approach to handle deeply nested structures efficiently and avoid Python's recursion limits. It is currently at version 0.4.7 and receives periodic updates focusing on features and maintenance.

Warnings

breaking This library requires Python 3.9 or newer. Users on older Python versions will encounter installation errors or runtime incompatibilities.
Fix: Upgrade your Python environment to 3.9 or newer.
gotcha The `logical-unification` library is a fork of the original `unification` project. While aiming for similar functionality, be aware that API or behavioral differences may exist. Ensure you are importing from `unification` (the installed package name for `logical-unification`) and not the original `unification` package if you intended to use this fork's features.
Fix: Verify that your `pip install` command is `pip install logical-unification` and your imports use `from unification import ...`.
gotcha Using `from unification import *` (wildcard import) as seen in some quickstart examples can pollute your namespace. For clarity and to avoid naming conflicts, it's generally recommended to import specific functions (e.g., `from unification import unify, var`).
Fix: Explicitly import the symbols you need: `from unification import unify, var, reify`.
gotcha Unification algorithms, by default or design choice, may or may not include an 'occurs check'. Omitting this check can lead to infinite terms (e.g., unifying `x` with `f(x)`), potentially causing infinite loops or memory exhaustion if not handled. While `logical-unification` uses a generator-based design to manage recursion, complex self-referential unifications might still behave unexpectedly if an explicit occurs check is not performed.
Fix: When performing complex unifications, especially with recursive data structures, be mindful of potential self-referential loops. Test thoroughly to understand the library's behavior in such edge cases.

Install

pip install logical-unification Install with pip

Imports

unify
```
from unification import unify
```
var
```
from unification import var
```
reify
```
from unification import reify
```
unifiable
```
from unification.core import unifiable
```

Quickstart

This quickstart demonstrates the core `unify` and `reify` functions, along with creating logic variables using `var()`. It shows how to unify basic Python types like integers and tuples, and how to apply the resulting substitutions to reify terms. Dictionaries are also supported for unification.

from unification import unify, var, reify

x = var()
y = var()

# Unify constants
print(f"Unify(1, 1): {unify(1, 1)}")
print(f"Unify(1, 2): {unify(1, 2)}")

# Unify with a variable
print(f"Unify((1, x), (1, 2)): {unify((1, x), (1, 2))}")

# Unify multiple variables where they must be the same
print(f"Unify((x, x), (1, 2)): {unify((x, x), (1, 2))}")

# Reify a term with a substitution
substitution = unify((1, x), (1, 2))
if substitution:
    print(f"Reify((1, x), {substitution}): {reify((1, x), substitution)}")

# Unify dictionaries
print(f"Unify({{\"a\": 1, \"b\": 2}}, {{\"a\": x, \"b\": 2}}): {unify({"a": 1, "b": 2}, {"a": x, "b": 2})}")

view raw JSON →