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