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

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.

Declarations

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.

Signature

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).

Definitions

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.

Terms

A term is either:

A declared variable x.
A function application f(t1, ..., tn), where f is a declared function symbol, and the $t_i$ are terms.

Formulas

A formula is either:

A declared propositional variable A.
A predicate application P(t1, ..., tn), where P is a declared predicate symbol, and the $t_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.

Examples

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)),
R(t,u),
P(u),
Q(t)

|- 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)

Docs