Procedures in Axi represent computations as opposed to deductions. Procedures are the things that most developers are familiar with already: a sequence of steps that produce some value as output.

Procedures in Axi are defined with the proc word (analogous to fn in Rust or function in JavaScript). The reason for this is that the function keyword in Axi has a different meaning (we will cover Axi's function later in the book).

Procedures can accept any values as input (including other procedures). This includes propositions, which can be useful for procedurally generating logical sentences:

Procedures can be used to encapsulate deductions as well. When a procedure's body ultimately evaluates a deduction, we refer to the procedure as a "tactic". Unlike computational procedures, tactics cannot return arbitrary values: they must return a conclusion. All of the deductive steps within the procedure's body must be logically sound. Axi will exit with an error if a procedure takes a malformed deductive step:

The following procedures proves a & b & c from a, b and c using a custom tactic called prove_and3.

Procedures can be nested and they follow the usual lexical scoping rules: