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 manysorted firstorder 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)
, wheref
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)
, whereP
is a declared predicate symbol, and the $t_i$ are terms whose types match the arity ofP
. 
A compound formula with one of the following logical connectives (in decreasing order of precedence):
~ A
for negationA && 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 universalexists <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)