semialg

Beta release: semialg 0.2.0b1 is a pre-release. APIs, solver coverage, result semantics, and performance characteristics may still change before 0.2.0 final. Exact/certified results are intended to preserve their documented contracts, but users should independently validate results for critical applications and report reproducible issues.

semialg is a Python package for exact symbolic computation with real polynomial and semialgebraic conditions. It combines cylindrical algebraic decomposition (CAD), quantifier elimination (QE), exact algebraic-number methods, and specialized solvers for decision problems, solving, regions, optimization, and integration.

The package is intended for research, education, and experimentation. Certified paths prefer an exact answer—or an explicit conservative failure—over silently treating a numerical approximation as proof.

Install

python -m pip install semialg

For development:

python -m pip install -e .[dev]

Quick start

import sympy as sp
from semialg import equivalent, implies, is_satisfiable

x, y = sp.symbols("x y", real=True)

is_satisfiable((x**2 + y**2 <= 1) & (x > 0) & (y > 0), [x, y])
# True

implies(x > 1, x**2 > 1, [x])
# True

equivalent(x**2 <= 1, (x >= -1) & (x <= 1), [x])
# True

First-order formulas can also be built directly with semialg's symbolic quantifiers:

from semialg import Exists, ForAll
from semialg.solve import reduce_complete_expr

statement = ForAll(x, Exists(y, sp.Eq(x + y, 0)))
reduce_complete_expr(statement)
# True

Optimization and integration use the same exact-first model:

from semialg import semialgebraic_minimize, semialgebraic_measure

opt = semialgebraic_minimize(x**2 + y**2, x + y >= 1, [x, y])
opt.value
# 1/2

semialgebraic_measure(x**2 + y**2 <= 1, [x, y])
# pi

What semialg provides

• Decision and QE: satisfiability, tautology, implication, equivalence, CAD and quantifier elimination.
• Solving and sampling: structured semialgebraic solutions, exact witnesses, CAD samples, and zero-dimensional RUR solving.
• Algebraic roots and parameters: exact root isolation, certified algebraic root functions, root classification, and parameter-stratified results.
• Regions: Boolean region operations, topology, connected components, standard geometric regions, and CAD-derived geometry.
• Optimization and ranges: exact polynomial optimization, KKT/active-set analysis, global certification, and semialgebraic image/range computation.
• Integration and moments: ambient and intrinsic measure, region integrals, moments, centroids, and covariance.

See the feature matrix for a more detailed capability summary and limitations for important scope boundaries.

Applied workflows

semialg.applications provides thin workflows built on the certified core:

• Robust parameter analysis — derive exact parameter regions for existential feasibility or universal satisfaction.
• Symbolic-math validation — certify identities, formula equivalence, and proposed function ranges.
• Optimization benchmark oracle — produce certified exact optima for checking numerical optimizers.
• Polynomial control stability — derive exact strict Hurwitz-stability regions from characteristic polynomials.
• Polynomial safety invariants — certify initiation, inductiveness, and unsafe-state exclusion for discrete polynomial systems.
• Polynomial response surfaces — compute exact extrema, ranges, gradients, and threshold regions for polynomial surrogate models.
• Polynomial model comparison — certify worst-case discrepancy, dominance, and equivalence over a domain.
• Parameter regime analysis — partition parameter space by solvability or real-root count.
• Polynomial probability — integrate exact polynomial densities over semialgebraic events and supports.

See docs/applications.md. Core operations such as function_range, semialgebraic_measure, integration, optimization, CAD, and QE remain in the core namespace rather than being duplicated under applications.

Semialg also includes thin certified application workflows for robust design, symbolic validation, optimization benchmarking, control stability, safety invariants, response surfaces, model comparison, parameter regimes, probability, Lyapunov/barrier verification, sensitivity analysis, and constraint diagnostics. See docs/applications.md.

Documentation

New users should start with Getting started and then follow the task-oriented links in the documentation index.

Important conceptual material:

• Exactness and certification
• Performance guide
• Errors and failure modes
• Symbol handling
• Region invariants
• API overview

A progressive executable tutorial is available in notebooks/semialg_demo.ipynb.

Exactness in one sentence

A result being symbolic is not by itself a certificate. semialg distinguishes exact representations, certified conclusions, candidate/heuristic information, and explicitly numerical approximations. See Exactness and certification.

Development

ruff format .
ruff check .
pytest -m "not slow"
pytest -m slow --durations=20
pytest -m performance --durations=20
python scripts/verify_source_quality.py

See architecture/design.md for implementation structure and CHANGELOG.md for release notes.

License

See LICENSE.

For release maturity and compatibility expectations, see docs/release_status.md.