API Reference

Complete reference for the logos public API.

Top-Level (`logos`)

`logos.var(name, type_) → Var`

Create a single symbolic variable.

x = logos.var("x", int)
print(x.name, x.type)   # x <class 'int'>

x <class 'int'>

`logos.vars(names, type_) → tuple[Var, ...]`

Create multiple variables from a space-separated string.

x, y, z = logos.vars("x y z", int)
print([v.name for v in [x, y, z]])  # ['x', 'y', 'z']

['x', 'y', 'z']

`logos.lit(value) → Lit`

Wrap a Python literal as an expression node.

from logos.expr import Lit
zero = logos.lit(0)
print(type(zero).__name__)   # Lit
print(zero.value)            # 0

Lit
0

`logos.forall(type_, ..., fn) → Expr`

Create a universally quantified statement from a lambda.

p = logos.forall(int, int, lambda x, y: x + y == y + x)
from logos.expr import ForallNode
print(type(p).__name__)  # ForallNode

ForallNode

`logos.exists(type_, fn) → Expr`

Create an existentially quantified statement from a lambda.

p = logos.exists(int, lambda x: x > logos.lit(5))
from logos.expr import ExistsNode
print(type(p).__name__)  # ExistsNode

ExistsNode

`@logos.theorem` — declare a theorem

Decorator that creates a Theorem object. No proof runs at declaration time.

@logos.theorem
def example_comm(x: int, y: int):
    return x + y == y + x

print(example_comm)              # Theorem[unverified]('example_comm')
print(example_comm.certified)   # False

Theorem[unverified]('example_comm')
False

`thm.proof(*tactics)` — attach a proof

Attach a proof spec and return self for chaining.

logos.check(example_comm.proof(t.intro("x", "y"), t.ring()))
print(example_comm.certified)   # True

True

`logos.check(thm) → thm`

Run the kernel. Marks thm.certified = True or raises LogosProofError.

@logos.theorem
def refl_thm(x: int):
    return x == x

logos.check(refl_thm.proof(t.intro("x"), t.refl()))
print(refl_thm.certified)   # True

True

`logos.prove(statement, proof_list) → _GroundProof`

Create a one-shot anonymous proof. Pass to logos.check() to validate.

gp = logos.prove(
    logos.forall(int, lambda x: x == x),
    [t.intro("x"), t.refl()],
)
logos.check(gp)
print(gp.certified)   # True

True

`@logos.axiom` — declare a trusted axiom

Decorator (or function call) that creates an Axiom object — trusted without proof.

@logos.axiom
def my_axiom(x: int):
    return x == x

print(my_axiom)             # Axiom('my_axiom')
print(my_axiom.certified)   # True

Axiom('my_axiom')
True

`logos.define`

Decorator that registers a symbolic function definition. Returns a Function object.

@logos.define
def double(x: int):
    return x + x

print(double(5))          # 10  (Python mode)
x = logos.var("x", int)
print(type(double(x)).__name__)  # App  (symbolic mode)
print(double.name)               # double

10
App
double

`logos.extern(name, arg_types, ret_type) → callable`

Declare an external uninterpreted function symbol.

my_fn = logos.extern("my_fn", [int], int)
x = logos.var("x", int)
from logos.expr import App
result = my_fn(x)
print(type(result).__name__)   # App

App

`logos.cases(*branches) → Expr`

Create a conditional expression for use inside @logos.define bodies.

x = logos.var("x", int)
expr = logos.cases(
    (x >= logos.lit(0), x),
    (x < logos.lit(0), -x),
)
from logos.expr import CaseExpr
print(type(expr).__name__)   # CaseExpr

CaseExpr

Expressions (`logos.expr`)

Class	Description	Example
`Var(name, type)`	Symbolic variable	`Var("x", int)`
`Lit(value)`	Literal value	`Lit(42)`
`Add(left, right)`	Addition	`x + y`
`Sub(left, right)`	Subtraction	`x - y`
`Mul(left, right)`	Multiplication	`x * y`
`Div(left, right)`	Integer division	`x // y`
`Mod(left, right)`	Modulo	`x % y`
`Neg(operand)`	Negation	`-x`
`Pow(base, exp)`	Power	`x ** 2`
`Eq(left, right)`	Equality	`x == y`
`Neq(left, right)`	Inequality	`x != y`
`Lt(left, right)`	Less-than	`x < y`
`Le(left, right)`	Less-or-equal	`x <= y`
`Gt(left, right)`	Greater-than	`x > y`
`Ge(left, right)`	Greater-or-equal	`x >= y`
`And(left, right)`	Conjunction	`p & q`
`Or(left, right)`	Disjunction	`p \\| q`
`Not(operand)`	Negation	`~p`
`Implies(ant, cons)`	Implication	`p >> q`
`ForallNode(var, body)`	Universal quantifier	`Forall(x, P)`
`ExistsNode(var, body)`	Existential quantifier	`Exists(x, P)`
`App(name, args)`	Function application	`double(x)`
`CaseExpr(branches)`	Case expression	`logos.cases(...)`

Tactics (`logos.tactics`)

Structural

Tactic	Description
`intro(*names)`	Strip `Forall`/`Implies`, add to context
`assumption()`	Close if goal is in context
`exact(term)`	Close with an explicit proof term
`apply(ref)`	Apply an Axiom/Theorem object or local hypothesis string
`split()`	`A & B` → `[A, B]`
`left(right_type)`	`A \\| B` → prove `A`
`right(left_type)`	`A \\| B` → prove `B`
`witness(val)`	`∃x.P(x)` → `P[x:=val]`
`contradiction()`	Close via `P` and `~P` in context

Arithmetic

Tactic	Description
`ring()`	Polynomial ring identities
`linarith()`	Linear arithmetic via Farkas
`decide()`	Evaluate ground boolean propositions

Rewriting

Tactic	Description
`refl()`	Prove `a == a`
`unfold(*refs)`	Replace function calls with definition bodies (accepts Function objects)
`rewrite(ref)`	Rewrite left-to-right using Axiom/Theorem object
`rewrite_rev(ref)`	Rewrite right-to-left
`eval_()`	Evaluate ground arithmetic sub-expressions
`norm_num()`	Normalize and close numeric ground goals

Combinators

Tactic	Description
`then(*tactics)`	Sequence tactics as one
`first(*tactics)`	Try each, succeed with first non-failing
`try_(tactic)`	Apply if possible, silent on failure
`repeat(tactic)`	Apply until failure
`all_goals(tactic)`	Apply tactic to each open subgoal

Kernel (`logos.kernel`)

The kernel is the only trusted code. Direct use is rare but available:

Proof Terms

Term	Proves
`Refl(e)`	`e == e`
`Symm(p)`	`b == a` (given `p: a==b`)
`Trans(p, q)`	`a == c` (given `p: a==b`, `q: b==c`)
`Subst(p, f)`	`f(a) == f(b)` (given `p: a==b`)
`Axiom(name)`	The named axiom’s statement
`HypRef(name)`	The named hypothesis
`ForallIntro(var, body)`	`∀x. P`
`ForallElim(proof, val)`	`P[x:=val]`
`ImpliesIntro(hyp, name, body)`	`P → Q`
`ImpliesElim(pq, p)`	`Q` (modus ponens)
`AndIntro(p, q)`	`A ∧ B`
`AndElimL(p)` / `AndElimR(p)`	`A` / `B`
`OrIntroL(p, right)` / `OrIntroR(left, p)`	`A ∨ B`
`CaseAnalysis(or_proof, name, left, right)`	Case split
`ExFalso(false_proof, conclusion)`	Ex falso quodlibet

Kernel Functions

from logos.kernel import infer, check, Context

# infer: determine what statement a proof term proves
stmt = infer(term, ctx)

# check: validate that term proves expected_stmt (raises KernelError on mismatch)
check(term, expected_stmt, ctx)

Helpers (`logos.helpers`)

from logos.helpers import structural_eq, substitute, free_vars

# structural_eq: recursively compare two expression trees
structural_eq(x + y, x + y)     # True
structural_eq(x + y, y + x)     # False

# substitute: replace all free occurrences of var with val
substitute(x + y, x, logos.lit(5))  # Lit(5) + y

# free_vars: names of free variables in an expression
free_vars(x + y)                 # {"x", "y"}
free_vars(Forall(x, x + y))      # {"y"}  (x is bound)

Exceptions

Exception	When raised
`logos.theorem.LogosProofError`	Proof fails in `logos.check`
`logos.runner.TacticFailed`	A tactic cannot proceed
`logos.kernel.KernelError`	Kernel rejects an invalid proof term

--- title: "API Reference" --- Complete reference for the logos public API. ```{python} #| echo: false import logos import logos.tactics as t ``` ## Top-Level (`logos`) ### `logos.var(name, type_) → Var` Create a single symbolic variable. ```{python} x = logos.var("x", int) print(x.name, x.type) # x <class 'int'> ``` ### `logos.vars(names, type_) → tuple[Var, ...]` Create multiple variables from a space-separated string. ```{python} x, y, z = logos.vars("x y z", int) print([v.name for v in [x, y, z]]) # ['x', 'y', 'z'] ``` ### `logos.lit(value) → Lit` Wrap a Python literal as an expression node. ```{python} from logos.expr import Lit zero = logos.lit(0) print(type(zero).__name__) # Lit print(zero.value) # 0 ``` ### `logos.forall(type_, ..., fn) → Expr` Create a universally quantified statement from a lambda. ```{python} p = logos.forall(int, int, lambda x, y: x + y == y + x) from logos.expr import ForallNode print(type(p).__name__) # ForallNode ``` ### `logos.exists(type_, fn) → Expr` Create an existentially quantified statement from a lambda. ```{python} p = logos.exists(int, lambda x: x > logos.lit(5)) from logos.expr import ExistsNode print(type(p).__name__) # ExistsNode ``` ### `@logos.theorem` — declare a theorem Decorator that creates a `Theorem` object. No proof runs at declaration time. ```{python} @logos.theorem def example_comm(x: int, y: int): return x + y == y + x print(example_comm) # Theorem[unverified]('example_comm') print(example_comm.certified) # False ``` ### `thm.proof(*tactics)` — attach a proof Attach a proof spec and return `self` for chaining. ```{python} logos.check(example_comm.proof(t.intro("x", "y"), t.ring())) print(example_comm.certified) # True ``` ### `logos.check(thm) → thm` Run the kernel. Marks `thm.certified = True` or raises `LogosProofError`. ```{python} @logos.theorem def refl_thm(x: int): return x == x logos.check(refl_thm.proof(t.intro("x"), t.refl())) print(refl_thm.certified) # True ``` ### `logos.prove(statement, proof_list) → _GroundProof` Create a one-shot anonymous proof. Pass to `logos.check()` to validate. ```{python} gp = logos.prove( logos.forall(int, lambda x: x == x), [t.intro("x"), t.refl()], ) logos.check(gp) print(gp.certified) # True ``` ### `@logos.axiom` — declare a trusted axiom Decorator (or function call) that creates an `Axiom` object — trusted without proof. ```{python} @logos.axiom def my_axiom(x: int): return x == x print(my_axiom) # Axiom('my_axiom') print(my_axiom.certified) # True ``` ### `logos.define` Decorator that registers a symbolic function definition. Returns a `Function` object. ```{python} @logos.define def double(x: int): return x + x print(double(5)) # 10 (Python mode) x = logos.var("x", int) print(type(double(x)).__name__) # App (symbolic mode) print(double.name) # double ``` ### `logos.extern(name, arg_types, ret_type) → callable` Declare an external uninterpreted function symbol. ```{python} my_fn = logos.extern("my_fn", [int], int) x = logos.var("x", int) from logos.expr import App result = my_fn(x) print(type(result).__name__) # App ``` ### `logos.cases(*branches) → Expr` Create a conditional expression for use inside `@logos.define` bodies. ```{python} x = logos.var("x", int) expr = logos.cases( (x >= logos.lit(0), x), (x < logos.lit(0), -x), ) from logos.expr import CaseExpr print(type(expr).__name__) # CaseExpr ``` --- ## Expressions (`logos.expr`) | Class | Description | Example | |-------|-------------|---------| | `Var(name, type)` | Symbolic variable | `Var("x", int)` | | `Lit(value)` | Literal value | `Lit(42)` | | `Add(left, right)` | Addition | `x + y` | | `Sub(left, right)` | Subtraction | `x - y` | | `Mul(left, right)` | Multiplication | `x * y` | | `Div(left, right)` | Integer division | `x // y` | | `Mod(left, right)` | Modulo | `x % y` | | `Neg(operand)` | Negation | `-x` | | `Pow(base, exp)` | Power | `x ** 2` | | `Eq(left, right)` | Equality | `x == y` | | `Neq(left, right)` | Inequality | `x != y` | | `Lt(left, right)` | Less-than | `x < y` | | `Le(left, right)` | Less-or-equal | `x <= y` | | `Gt(left, right)` | Greater-than | `x > y` | | `Ge(left, right)` | Greater-or-equal | `x >= y` | | `And(left, right)` | Conjunction | `p & q` | | `Or(left, right)` | Disjunction | `p \| q` | | `Not(operand)` | Negation | `~p` | | `Implies(ant, cons)` | Implication | `p >> q` | | `ForallNode(var, body)` | Universal quantifier | `Forall(x, P)` | | `ExistsNode(var, body)` | Existential quantifier | `Exists(x, P)` | | `App(name, args)` | Function application | `double(x)` | | `CaseExpr(branches)` | Case expression | `logos.cases(...)` | --- ## Tactics (`logos.tactics`) ### Structural | Tactic | Description | |--------|-------------| | `intro(*names)` | Strip `Forall`/`Implies`, add to context | | `assumption()` | Close if goal is in context | | `exact(term)` | Close with an explicit proof term | | `apply(ref)` | Apply an Axiom/Theorem object or local hypothesis string | | `split()` | `A & B` → `[A, B]` | | `left(right_type)` | `A \| B` → prove `A` | | `right(left_type)` | `A \| B` → prove `B` | | `witness(val)` | `∃x.P(x)` → `P[x:=val]` | | `contradiction()` | Close via `P` and `~P` in context | ### Arithmetic | Tactic | Description | |--------|-------------| | `ring()` | Polynomial ring identities | | `linarith()` | Linear arithmetic via Farkas | | `decide()` | Evaluate ground boolean propositions | ### Rewriting | Tactic | Description | |--------|-------------| | `refl()` | Prove `a == a` | | `unfold(*refs)` | Replace function calls with definition bodies (accepts Function objects) | | `rewrite(ref)` | Rewrite left-to-right using Axiom/Theorem object | | `rewrite_rev(ref)` | Rewrite right-to-left | | `eval_()` | Evaluate ground arithmetic sub-expressions | | `norm_num()` | Normalize and close numeric ground goals | ### Combinators | Tactic | Description | |--------|-------------| | `then(*tactics)` | Sequence tactics as one | | `first(*tactics)` | Try each, succeed with first non-failing | | `try_(tactic)` | Apply if possible, silent on failure | | `repeat(tactic)` | Apply until failure | | `all_goals(tactic)` | Apply tactic to each open subgoal | --- ## Kernel (`logos.kernel`) The kernel is the only trusted code. Direct use is rare but available: ### Proof Terms | Term | Proves | |------|--------| | `Refl(e)` | `e == e` | | `Symm(p)` | `b == a` (given `p: a==b`) | | `Trans(p, q)` | `a == c` (given `p: a==b`, `q: b==c`) | | `Subst(p, f)` | `f(a) == f(b)` (given `p: a==b`) | | `Axiom(name)` | The named axiom's statement | | `HypRef(name)` | The named hypothesis | | `ForallIntro(var, body)` | `∀x. P` | | `ForallElim(proof, val)` | `P[x:=val]` | | `ImpliesIntro(hyp, name, body)` | `P → Q` | | `ImpliesElim(pq, p)` | `Q` (modus ponens) | | `AndIntro(p, q)` | `A ∧ B` | | `AndElimL(p)` / `AndElimR(p)` | `A` / `B` | | `OrIntroL(p, right)` / `OrIntroR(left, p)` | `A ∨ B` | | `CaseAnalysis(or_proof, name, left, right)` | Case split | | `ExFalso(false_proof, conclusion)` | Ex falso quodlibet | ### Kernel Functions ```python from logos.kernel import infer, check, Context # infer: determine what statement a proof term proves stmt = infer(term, ctx) # check: validate that term proves expected_stmt (raises KernelError on mismatch) check(term, expected_stmt, ctx) ``` --- ## Helpers (`logos.helpers`) ```python from logos.helpers import structural_eq, substitute, free_vars # structural_eq: recursively compare two expression trees structural_eq(x + y, x + y) # True structural_eq(x + y, y + x) # False # substitute: replace all free occurrences of var with val substitute(x + y, x, logos.lit(5)) # Lit(5) + y # free_vars: names of free variables in an expression free_vars(x + y) # {"x", "y"} free_vars(Forall(x, x + y)) # {"y"} (x is bound) ``` --- ## Exceptions | Exception | When raised | |-----------|-------------| | `logos.theorem.LogosProofError` | Proof fails in `logos.check` | | `logos.runner.TacticFailed` | A tactic cannot proceed | | `logos.kernel.KernelError` | Kernel rejects an invalid proof term |

Top-Level (logos)

logos.var(name, type_) → Var

logos.vars(names, type_) → tuple[Var, ...]

logos.lit(value) → Lit

logos.forall(type_, ..., fn) → Expr

logos.exists(type_, fn) → Expr

@logos.theorem — declare a theorem

thm.proof(*tactics) — attach a proof

logos.check(thm) → thm

logos.prove(statement, proof_list) → _GroundProof

@logos.axiom — declare a trusted axiom

logos.define

logos.extern(name, arg_types, ret_type) → callable

logos.cases(*branches) → Expr

Expressions (logos.expr)

Tactics (logos.tactics)