Welcome to Axi

Axi is a powerful deductive programming language for proof engineering and formal software development.

Key Features

1. Familiar syntax and language features reduces the barrier of entry for developers who lack formal methods experience.
2. Deductive programs generate proofs-as-traces, which are machine-checkable certificates of an Axi program's output
3. Write custom tactics (encapsulated, reusable proof procedures) as easily as normal functions
4. Programming and deduction can be mixed together seamlessly without sacrificing the soundness of formal proofs
5. Powerful pattern matching
6. Support for inductive data structures and inductive proofs.
7. Support for equational reasoning and rewrite logic

Propositional Logic

Axi supports reasoning in the natural deduction style. We will declare some opaque propositions to reason about. Later we'll see that they are actually constant terms of a special type Boolean when we talk about first-order logic.

There is a global assumption base that contains all the axioms and all the theorems that have been proved so far.

The following assume block proves $p \to q$.

It does this by inserting p into the assumption base and then proving q within that context. After the block is finished, p and anything proved in the block will be removed from the assumption base. A final conclusion should be proved by the block. Let's say it's q, then $p \to q$ is proved by the whole assume block and added to the assumption base.

Basic Proof Rules

Expressions preceded with the bang operator (!) indicate that the expression is an invocation of a tactic. Tactics in proof development are analogous to functions in programming: they encapsulate reusable sequences of steps behind an easily callable interface. While functions encapsulate a series of computations, tactics encapsulate a series of deductive steps. Tactics terminate successfully only if the tactic's deductive steps are all valid relative to the assumption base that is present during the tactic's evaluation. Every tactic (indeed every deduction in Axi) produces a conclusion, and the conclusion is added to the outer scope's assumption base.

Below is a deduction that proves that $\neg \neg a \to a$ using the tactic dn (double-negation).

Axi comes with built in tactics for each of the deductive rules in propositional logic, including the introduction and elimination rules for each of the logical connectives.

Below, the introduction and elimination rules are demonstrated for conjunction, disjunction, implication and equivalence, as well as deductive rules such as modus ponens.