Syntax guide

This guide explains how to write your own goals to prove, using a homemade ASCII syntax tailored for the logic of Actema.


Goals are specified with the following syntax:

<decl>, ..., <decl>; <form>, ..., <form> |- <form>

where the <decl> are declarations of symbols and definitions (see next section), the <form> on the left of |- are the hypotheses of the goal, and the <form> on the right of |- is the conclusion to be proved.


The current prototype of Actema is based on many-sorted first-order intuitionistic logic. In this context, declarations have two purposes:

  • Specifying the signature of the theory under consideration, that is the primitive sorts/types as well as function and predicate symbols with their arities;

  • Adding definitions for compound types, terms and predicates.


You can declare 5 kinds of objects in the signature of a theory:

  • Primitive types type <ident>, where <ident> is an identifier starting with a letter (e.g. nat, bool, IntList, Foobar...)

  • Term variables <ident> : <type>, where <type> is either a builtin or previously declared type (e.g. n : nat)

  • Functions <ident> : <type> & ... & <type> -> <type>, with the arguments types on the left of -> and the return type on the right (e.g. plus : nat & nat -> nat)

  • Propositional variables <ident> (e.g. A, B, C...)

  • Atomic predicates <ident> :: <type> & ... & <type>, where the list of <type> corresponds to the arity of the predicate (e.g. equals :: nat & nat)

As suggested by the previous examples, there is a builtin signature for Peano arithmetic, with the following entries:

type nat,

zero : -> nat,
succ : nat -> nat,
plus : nat & nat -> nat,
mult : nat & nat -> nat,

_EQ :: nat & nat

Note: there is syntactic sugar for the equality predicate _EQ: you can write n = m instead of _EQ(n, m).


To avoid manipulating directly complex expressions, Actema supports a mechanism of definitions to name the various objects in a development:

  • type <ident> := <type> defines a type alias.

  • <ident> := <term> defines a term alias (see next section for how to build complex terms). The same syntax is used when adding a new term alias with the green +expr button in the course of a proof.

  • There is currently no support for predicate definitions.

Terms and formulas

Once the signature of the theory is fixed, we can start building complex terms and formulas.


A term is either:

  • A declared variable x.

  • A function application f(t1, ..., tn), where f is a declared function symbol, and the tit_i are terms.


A formula is either:

  • A declared propositional variable A.

  • A predicate application P(t1, ..., tn), where P is a declared predicate symbol, and the tit_i are terms whose types match the arity of P.

  • A compound formula with one of the following logical connectives (in decreasing order of precedence):

    • ~ A for negation
    • A && B for conjunction (left associative)
    • A || B for disjunction (left associative)
    • A -> B for implication (right associative)
    • A <-> B for equivalence (right associative)
  • A quantified formula:

    • forall <ident> : <type> . <form> for the universal
    • exists <ident> : <type> . <form> for the existential

Note: you can add parentheses to disambiguate an unclear precedence of operators.


Propositional calculus

A, B, C |- (A || B -> C) <-> (A -> C) && (B -> C)

Predicate calculus

R :: () & (), P :: (), Q :: (), t : (), u : ();

(forall x : (). forall y : (). R(x,y) -> R(y,x)),

|- exists a : (). exists b : (). R(a,b) && P(a) && Q(b)

Peano arithmetic


forall x : nat. ~(Z() = S(x)),
forall x : nat. forall y : nat. S(x) = S(y) -> x = y,
forall x : nat. add(x, Z()) = x,
forall x : nat. forall y : nat. add(x, S(y)) = S(add(x, y)),
forall x : nat. mult(x, Z()) = Z(),
forall x : nat. forall y : nat. mult(x, S(y)) = add(mult(x, y), x)

|- forall x : nat. forall y : nat. add(x, y) = add(y, x)