agent-logic is a modular Python library for constructing, evaluating, transforming, and proving logical expressions — a lightweight symbolic logic + SAT engine designed for LLM‑driven agent systems.
Structured. Serializable. Reasonable. Agent‑Ready.
It enables:
- ✅ Propositional Logic —
AND,OR,NOT,IMPLIES,IFF - ✅ Predicate Logic — Terms, Predicates, Quantifiers (
∀,∃) - ✅ Formal Proof Validation — inference rules & structured derivations
- ✅ Truth Tables & Satisfiability — tautology / contradiction checks
- ✅ Logical Transformations — equivalences, CNF/DNF (where applicable)
- ✅ AST Parsing — recursive, typed abstract syntax trees
- ✅ Type‑Safe Models — Pydantic v2 schemas for strict, serializable I/O
- 🔜 SAT Backbone — CNF conversion + DPLL/modern SAT (in progress)
🔗 Works great as a structured tool for LLMs (LangChain/OpenAI Tools/JSON Mode).
- Core symbolic logic (propositions, connectives, predicates, quantifiers) — implemented.
- Truth tables, tautology/contradiction checking, core proof validation — working & tested.
- Inference rules (e.g., Modus Ponens, Modus Tollens, HS, Dilemmas, ↔ elimination) — available.
- AST parsing, SAT‑based search, deeper quantifier handling — in progress.
⚠️ Advanced quantifier transformations and large proof automation are under active development.
pip install agent-logic
# or from source
git clone https://github.com/pr1m8/agent-logic.git
cd agent-logic
poetry installDesign goals
- Explicit structure over strings; runtime‑validatable (Pydantic v2)
- Deterministic evaluation; pure, testable transforms
- LLM‑friendly: JSON‑serializable nodes, strict enums, Literals
Core types (illustrative)
# agent_logic/core/ast.py (conceptual)
from pydantic import BaseModel
from typing import Literal, List, Optional
class Proposition(BaseModel):
name: str
class UnaryOp(BaseModel):
operator: Literal["NOT"]
operand: "Expression"
class BinaryOp(BaseModel):
operator: Literal["AND","OR","IMPLIES","IFF"]
left: "Expression"
right: "Expression"
class Quantifier(BaseModel):
kind: Literal["FORALL","EXISTS"]
var: str
body: "Expression"
Expression = Proposition | UnaryOp | BinaryOp | QuantifierAll nodes are JSON‑serializable and suitable for structured outputs.
from agent_logic.core.operations import Proposition, BinaryOp
from agent_logic.evaluation.truth_table import TruthTable
# Define propositions
p = Proposition(name="P")
q = Proposition(name="Q")
# (P AND Q)
expr = BinaryOp(left=p, right=q, operator="AND")
# Truth table
table = TruthTable(expression=expr)
for row in table.generate():
print(row)
print("Is tautology:", table.is_tautology())
print("Is contradiction:", table.is_contradiction())Output (sketch):
P Q | P∧Q
0 0 | 0
0 1 | 0
1 0 | 0
1 1 | 1
Is tautology: False
Is contradiction: False
from agent_logic.core.operations import Predicate, Quantified
# ∀x. Likes(x, Pizza) → Exists y. Likes(y, Pizza)
forall_likes = Quantified.forall(
var="x",
body=Predicate(name="Likes", terms=["x","Pizza"])
)
exists_liker = Quantified.exists(
var="y",
body=Predicate(name="Likes", terms=["y","Pizza"])
)
implication = forall_likes >> exists_liker # syntactic sugar for IMPLIES- Variable scoping and capture‑avoiding substitution are handled in the model layer.
- Advanced transformations (Skolemization/Unification) planned.
Supported rules (subset):
- MP (Modus Ponens), MT (Modus Tollens)
- HS (Hypothetical Syllogism), DS (Disjunctive Syllogism)
- Constructive / Destructive Dilemmas
- ↔‑Elimination, →‑Elimination/Introduction
- ∧‑Introduction/Elimination, ∨‑Introduction
- Quantifier rules (intro/elimination) — basic forms
Derivation sketch:
from agent_logic.proof.rules import modus_ponens, biconditional_elim
from agent_logic.proof.derivation import Derivation
D = Derivation()
D.assume("P")
D.assume("P -> Q")
D.apply(modus_ponens, "P", "P -> Q") # yields Q
D.qed(target="Q")The proof engine enforces well‑typed steps, tracks line references, and can export structured proof objects.
TruthTable(expr).is_tautology()and.is_contradiction()satisfiable(expr)and model enumeration (bounded)- CNF/DNF transforms where applicable; full SAT (DPLL/modern) in progress
- De Morgan, Double Negation, Implication/Biconditional Elimination
- Normal Forms (CNF/DNF) where defined
- Alpha‑equivalence for predicate logic (variable renaming)
- Propositional & Predicate Logic Core
- Truth Tables & Tautology Checking
- Structured Proof Validation Engine
- Advanced SAT Solving (CNF + DPLL/modern)
- Quantifier Manipulation (Skolemization, Unification)
- NL → Formal Logic Parsing (experimental)
- Web Visualizer Playground
agent_logic/
├── core/
│ ├── ast.py # Node definitions
│ ├── operations.py # Constructors, sugar, helpers
├── evaluation/
│ ├── truth_table.py # Table + tautology/contradiction
│ └── satisfiability.py # Model search (bounded), CNF helpers
├── transform/
│ └── normalize.py # CNF/DNF, equivalences
├── proof/
│ ├── rules.py # Inference rules
│ ├── derivation.py # Proof objects & checking
│ └── checker.py # Validation engine
├── parsing/
│ ├── parser.py # (planned) from strings to AST
│ └── printer.py # pretty printers / LaTeX
├── integrations/
│ └── tools.py # LangChain/OpenAI Tools wrappers
└── tests/
git clone https://github.com/pr1m8/agent-logic.git
cd agent-logic
poetry install
poetry run pytest -qQuality & style:
- Tests:
pytest -q - Lint:
ruff format .+ruff check . - Types:
pyrightormypy - Docs: Google‑style docstrings; examples for public APIs
Contributions are welcome! Please:
- Open an issue to discuss substantial changes
- Keep PRs focused; include tests and examples
- Follow typing and modeling patterns (Pydantic v2)
See CONTRIBUTING.md and CODE_OF_CONDUCT.md.
MIT License — see LICENSE.
Empower your agents with true reason.
“Teach your models to reason, not just predict.”