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).
Predicated (a special case of interpreted functions).
logic: uninterpreted symbols¶
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
Please refer to section Types for more information on the types of symbols that can be created.
<logic_declaration> ::= "logic" <identifier_list> ":" <type> <identifier_list> ::= <identifier> ( "," <identifier> )*
(* 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.
<logic_ac_declaration> ::= "logic" "ac" <identifier_list> ":" <type> <identifier_list> ::= <identifier> ( "," <identifier> )*
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¶
function keyword, the user can add its own (interpreted) functions.
<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>
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¶
predicate construct allows to user to define (interpreted) functions whose codomain is of type
It is possible to create “ground predicates”, i.e. predicates with no arguments.
Since Alt-Ergo 2.3.0,
bool have the same behaviour:
predicate can therefore be seen as a shorthand for as boolean-valued
See section Types for more information on the
<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>
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)