# Declaration of symbols¶

In order to introduce the problem’s vocabulary, the user can declare its own symbols.

• Simple variables and uninterpreted functions.

• Associative and commutative symbols (a special case of uninterpreted functions).

• Interpreted functions.

• Predicated (a special case of interpreted functions).

## `logic`: uninterpreted symbols¶

The `logic` keyword allows the user to define new uninterpreted (typed) symbols. Those symbols may be used to represent simple variables, uninterpreted functions, data structures, … Constraints on those symbols may be added via the `axiom` keyword.

Please refer to section Types for more information on the types of symbols that can be created.

### Syntax¶

```<logic_declaration> ::= "logic" <identifier_list> ":" <type>
<identifier_list>   ::= <identifier> ( "," <identifier> )*
```

### Examples¶

```(* Introducing propositional variables *)
logic p,q,r: prop

axiom a: p and q -> r
goal g: p -> r
```
```(* Introducing uninterpreted functions *)
logic f: int -> int
axiom a1: forall x:int. f(x)>0
goal g1: f(1)>=0
```
```(* Functions can have multiple arguments *)
logic h, g, f: int, int -> int
logic a, b: int

goal g_2 :
h(g(a,a),g(b,b)) = g(b,b) ->
a = b ->
g(f(h(g(a,a),g(b,b)),b) - f(g(b,b),a),
f(h(g(a,a),g(b,b)),a) - f(g(b,b),b)) = g(0,0)
```
```(* Axioms can be used to add constraints *)
logic Ack: int, int -> int
axiom Ack_n:
forall n:int.
Ack(0,n)=n+1
axiom Ack_m:
forall m:int. m>0 ->
Ack(m,0) = Ack(m-1,1)
axiom Ack_nm:
forall n,m:int. n>0 -> m>0 ->
Ack(m,n) = Ack(m-1,Ack(m,n-1))
```

## `ac` modifier: associative and commutative symbols¶

When creating a new uninterpreted symbol trough the `logic` keyword, the user can add the `ac` modifier to inform Alt-Ergo that this symbol is associative and commutative (AC). Using this symbol makes it possible to take advantage of Alt-Ergo’s built-in support for AC-symbols.

Most automated theorem provers have difficulties in handling associative and commutative symbols. It is indeed possible to write

```logic f: int, int -> int
axiom associative: forall x,y,z:int. f(f(x,y),z) = f(x,f(y,z))
axiom commutative: forall x,y:int. f(x,y) = f(y,x)
```

However, handling universally-quantified axioms is challenging for this kind of solvers. It is necessary to create ‘instances’ of those axioms in order to use them, and the number of instances can quickly become overwhelming.

In Alt-Ergo’s native language, one can simply write

```logic ac f: int, int -> int
```

in order to specify that `f` is an AC-symbol. Once this is done, Alt-Ergo will use the built-in AC(X) algorithm to handle this symbol much more efficiently than what would have been possible through axioms.

### Syntax¶

```<logic_ac_declaration> ::= "logic" "ac" <identifier_list> ":" <type>
<identifier_list>      ::= <identifier> ( "," <identifier> )*
```

### Examples¶

```type person
(* Last common ancestor *)
logic ac lca: person, person -> person
logic Alice, Bob, Eve: person

goal g: lca(Alice, lca(Bob, Eve)) = lca(Eve, lca(Alice, Bob))
```
```logic ac u: int, int -> int
goal g1: u(1,u(2,u(3,u(4,5)))) = u(u(u(u(5,4),3),2),1)
goal g2: forall a,b,c,v,w:int. u(a,b) = w and u(a,c) = v -> u(b,v) = u(c,w)
```

## `function`: user-defined functions¶

Using the `function` keyword, the user can add its own (interpreted) functions.

### Syntax¶

```<function_declaration>    ::= "function" <function_id> "(" <function_parameter_list> ")" ":" <output_type> "=" <function_body>
<function_parameter_list> ::= <function_parameter> ( "," <function_parameter> )*
<function_parameter>      ::= <parameter_id> ":" <parameter_type>
<function_body>           ::= <expression>
```

### Examples¶

```function abs(x:int):int =
if x>=0 then (x) else (-x)

goal g: forall x:int. abs(x)>=0
```
```type person
logic father_of: person, person -> prop
logic mother_of: person, person -> prop

function son_of(kid:person, parent:person):bool =
father_of(parent, kid) or mother_of(parent, kid)
```

## `predicate`: propositional valued functions¶

The `predicate` construct allows to user to define (interpreted) functions whose codomain is of type `prop`.

It is possible to create “ground predicates”, i.e. predicates with no arguments.

Since Alt-Ergo 2.3.0, `prop` and `bool` have the same behaviour: `predicate` can therefore be seen as a shorthand for as boolean-valued `function`. See section Types for more information on the `prop`/`bool` keywords.

### Syntax¶

```<predicate_declaration>    ::= "predicate" <predicate_id> ( "(" <predicate_parameter_list> ")" )? "=" <predicate_body>
<predicate_parameter_list> ::= <predicate_parameter> ( "," <predicate_parameter> )*
<predicate_parameter>      ::= <predicate_id> ":" <predicate_type>
<predicate_body>           ::= <expression>
```

### Examples¶

```type person
logic father_of: person, person -> prop
logic mother_of: person, person -> prop

predicate son_of(kid:person, parent:person) =
father_of(parent, kid) or mother_of(parent, kid)
```