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>
<decl> are declarations of symbols and definitions (see next
<form> on the left of
|- are the hypotheses of the goal, and
<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:
type <ident>, where
<ident>is an identifier starting with a letter (e.g.
<ident> : <type>, where
<type>is either a builtin or previously declared type (e.g.
n : nat)
<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)
<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
n = m instead of
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
+exprbutton 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
A function application
f(t1, ..., tn), where
fis a declared function symbol, and the are terms.
A formula is either:
A declared propositional variable
A predicate application
P(t1, ..., tn), where
Pis a declared predicate symbol, and the are terms whose types match the arity of
A compound formula with one of the following logical connectives (in decreasing order of precedence):
~ Afor negation
A && Bfor conjunction (left associative)
A || Bfor disjunction (left associative)
A -> Bfor implication (right associative)
A <-> Bfor 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.
A, B, C |- (A || B -> C) <-> (A -> C) && (B -> C)
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)
; 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)