Axioma — a programming language for reasoning

The language, in six axioms

What you can say

Axioma reads like mathematics and runs like a program. Each construct below is real, executable syntax — try any of it in the playground.

I.

Sets are first-class

Set-builder notation, comprehensions, and the full algebra of sets — straight from the page into the runtime.

nums: [1, 2, 3, 4, 5, 6]
{ n | n <- nums, n mod 2 == 0 }  ⇒ {2, 4, 6}

II.

Logic is executable

Universal and existential quantifiers range over sets and evaluate to a truth value — ∀ and ∃, as code.

forall x in {2, 4, 6} | x mod 2 == 0   ⇒ true
exists x in {1, 2, 3} | x > 2        ⇒ true

III.

Rules reason for you

Declare facts and Horn-clause rules; recursion computes the full transitive closure, Datalog-style.

ancestor(X, Z) :- parent(X, Z)
ancestor(X, Z) :- parent(X, Y) and ancestor(Y, Z)

IV.

Truth has more than two values

Boolean, Kleene K3, Łukasiewicz L3, Belnap B4, and Gödel G3 — first-class logics for the unknown and the contradictory.

belnap("both")   ⇒ ⊤⊥
om or true        ⇒ true   # unknown ∨ true

V.

“is” means three things

Russell's copula, made precise: identity, predication, and existence — with concepts, instances, and classification.

concept Stock { price: 0 }
aapl: a Stock { price: 150 }
aapl is Stock     ⇒ true

VI.

Reasoning runs anywhere

The whole interpreter compiles to WebAssembly — no install, no server. It also speaks Forth-style stacks and prose-like definitions.

# a function, REBOL-style binding
sq: func(n) [n * n]
map(sq, [1, 2, 3])     ⇒ [1, 4, 9]

Many-valued logic

Beyond true and false

Real knowledge is incomplete and sometimes contradictory. Axioma builds that in: Belnap's four-valued bilattice treats missing and conflicting information as first-class truth values.

⊤ true asserted, no conflict
⊥ false denied, no conflict
⊤⊥ both asserted and denied — a paraconsistent contradiction
? neither no information either way

Contradiction propagates through rules instead of crashing — and every derived fact carries its epistemic grounding, from axiom down to hypothesis.

A cognitive paradigm

Computing as the mind does

Axioma is a cognitive programming language — built for knowledge representation, symbolic reasoning, and explainable AI. After procedural, object-oriented, functional, and logic programming comes a fifth paradigm, whose defining act is to understand: to model a thing into a model of everything. Seventeen logics and eight knowledge-representation systems, unified under a single old dream.

“Calculemus. Let us calculate.”— G. W. Leibniz, on settling every dispute by computation

1679

Leibniz

characteristica universalis + calculus ratiocinator — a universal language of thought, and a calculus to reason in it.

1854

Boole

The Laws of Thought — the algebra of logic.

1879

Frege

Begriffsschrift — the first formal logic; quantifiers, sense & reference.

1903

Russell

Types, definite descriptions, and the three meanings of “is.”

1931

Gödel

Incompleteness — and numbering a formal system within itself.

1959

McCarthy

Programs with common sense.

today

Axioma

The cognitive language — 17 logics and 8 knowledge-representation systems, executable in your browser.