1.1
(1)Variables变量被赋值后，称为一个常项。
常量被赋值后，便不能被其他数据赋值。
变量：用于表示暂时不能命名或者不需要命名的对象，用大写字母开头。
eg: APayloadInteger.Icom.betfair.prova.domain.Market.M
(2)Constants eg: 12, ‘test’, “test”
global constants : eg: $Count.addAndGet(Delta)
(3)Compound terms(lists)
格式：[Head|Rest](Head是列表开始元素（一个或多个元素，以逗号隔开）Rest 是列表尾部，常是一个变量)

(4)Facts
是一个元组关系，元组可为任意项：常量，变量或为(循环)列表格式：predicate(arg1,、、、,argn) eg: alert_destination(no_bids, store_manager)
格式：<谓词名>(<项表>).
功能：一般表示对象的性质或关系。
其中谓词名是以小写字母打头的字母、数字、下划线等组成的字符串，项表是以逗号隔开的项序列。
例如：
student(john).like(mary,music).
表示”约翰是学生“和”玛丽喜欢音乐“。

(5)Rules
Prova rules typically are Horn rules that are first‐order disjunctions of literals with exactly one positive literal. In logics, such Horn rules are known as definite clauses.

Reactive rules:
IF conditions A1,...,An is true, then perform action B.

格式：
head_literal(args_h):-
body_literal1(args_1),
…,
body_literaln(args_n).
‘：-’is pronounced as IF.
格式：
<谓词名>(<项表>):-<谓词名>(<项表>){,<谓词名>(<项表>)}.
功能：一般表示对象间的因果关系、蕴含关系或对应关系。
其中":-"表示"if",其左部的谓词是规则的结论(头)，右部的谓词是规则的前提，{}表示零次或多次重复，逗号表示and（逻辑与），即规则的形式是一个逻辑蕴含式。
例如：
bird(X):-animal(X),has(X,feather).
grandfather(X,Y):-father(X,Z),father(Z,Y).
第一条规则表示”如果X是动物，并且有羽毛，则X是鸟“；
第二条规则就表示”X是Y的祖父，如果存在Z, X是Z的父亲并且Z又是Y的父亲“。

例子：
is_a("anticoagulant","molecular_function").
% Rules (how to derive new knowledge)
parent(X,Y) :- % X is parent of Y IF Y is a (kind of) X
is_a(Y,X).
parent(X,Y) :- % X is parent of Y IF X has a Y
has_a(X,Y).
% Goal (what to do/what to derive)
% Who is Parent of "anticoagulant"?
:- solve(parent(Parent,Son)).

1.5
Expressions
(1)Arithmetic expressions:
expr: aterm((PLUS|MINUS) expr)?;
aterm :(MINUS?variable|number|MINUS?
predicate_java_call|OPEN expr CLOSE)((MULT|DIV|REM)aterm)?;

例子：
:-solve(expr001(N,3)).
expr001(N,M) :-
println(["==========expr001=========="]),
N=M+1*2.
expr001(N,M) :-
N=-M+1*-2.
expr001(N,M) :-
N=(-M+1)*-2.

1.6
Global constants
语法：
$Var=<rhs>
eg: globals001.prova
% Prova 3.0
% Demonstrating globals.
% $A is set initially to 'a' in ProvaGlobalsTest.globals001(). So two solutions here: 1 and 2.
%最终结果要返回到N中
:- solve(globals(N)).
globals(N) :-
%data($A,N).与data(a,1).进行匹配=》$A=a,N=1
%结束此次匹配
data($A,N).
globals(N) :-
%$A初始化为b
$A=b,
%?data($A,N)与data(b,2).进行匹配,推出N=2,此为最终结果
data($A,N).
data(a,1).
data(b,2).

1.7
Prova maps for defining
slotted termsSlotted terms is a highly valuable feature of languages like
Frame-Logic, standards(RIF or RuleML), and products.
eg: map2.prova
:- solve(own(X)).
buy({buyer->'Bill',seller->'Amazon',item->'Avatar Blu-ray'}).
keep({keeper->'Bill',item->'Avatar Blu-ray'}).
own({owner->Person,item->Object}) :-
buy({buyer->Person,seller->Merchant,item->Object}),
keep({keeper->Person,item->Object}).

例子：
@label(rule1) r1(X):-q(X).
@label(rule2) r2(X):-q(X).
@label(rule3) r2(X):-q(X).
q(1).
q(2).
q(3).
:-solve(r1(X1)).
% scoped with label "rule1"
p1(X):-
@label(rule1)
r1(X).
:-solve(p1(X2)).
% fails since scope is "rule2"
p2(X):-
@label(rule2)
r1(X).
:-solve(p2(X3)).
% succeeds since scope is EITHER "rule2" OR "rule1"
p2a(X):-
@label(rule2,rule1)
r1(X).
:-solve(p2a(X4)).
% match AND get rule label for the rule that matched
p3(X,Y):-
@label(Y)
r1(X).
:-solve(p3(X5,Label5)).
% match AND get rule label for the rule that matched
p4(X,Y):-
@label(Y)
r2(X).
:-solve(p4(X6,Label6)).
% dynamically set the metadata value expected from matching rules
:-solve(p4(X7,rule2)).
% get module label
p5(X,Y):-
@src(Y) @label(rule1)
r1(X).
:-solve(p5(X8,Src8)).
% get module label
p6(X,Y):-
@src(Y) @label(rule3)
r2(X).
:-solve(p6(X9,Src9)).

Metadata is a set of annotations each of which is a pair defined as :
@key(value [,value]*).
Both keys and values are arbitary strings defined by their occurrence in an annotation.

1.9
Guards in Prova

例子：
@author(dev1) r1(X):-q(X).
@author(dev22) r2(X):-q(X).
@author(dev32) r2(X):-s(X).
q(2).
s(-2).
trusted(dev1).
trusted(dev22).
% Author dev22 is trusted but dev32 is not, so one solution is found: X1=2
p1(X):-
@author(A)
r2(X) [trusted(A)].
:-solve(p1(X1)).
a(X):-qq(X).
a(X):-s(X).
% This example shows how guards can be used to implement a "dynamic CUT".
% The CUT in the guard is dynamically spliced into the start of the target rule body.
% As qq(X) has no solutions, the CUT prevents further backtracking to the second rule for a(X):-s(X),
% that would have yielded a solution but does not due to that dynamic CUT.
p2(X):-
a(X) [!].
:-solve(p2(X2)).
% Demonstrate a guarded reaction. The server looks for logins for one user from different IP addresses.
% The guard on the second reaction filters the expected follow-up message.
% This will print:
% user2 30.30.30.30 40.40.40.40
:- eval(server()).
% eval 重新运算求出参数的内容
server() :-
% Start detection on each new login
rcvMult(XID,Protocol,From,request,login(User,IP)),
% Wait for a right follow-up while ignoring anything that does not match
@timeout(1000)
rcvMsg(XID,Protocol,From,request,login(User,IP2)) [IP2!=IP],
% Once the full match has occurred, the above rcvMsg reaction is removed
$Count.incrementAndGet(),
println([User,IP,IP2]," ").
:- eval(client()).
client() :-
% Send all the test messages from a separate thread
switch_thread(),
sendMsg(XID,user1,0,request,login(user1,'10.10.10.10')),
% Wait synchronously, could have waited asynchronously instead
java.lang.Thread.sleep(500L),
sendMsg(XID,user2,0,request,login(user2,'30.30.30.30')),
java.lang.Thread.sleep(700L),
sendMsg(XID,user1,0,request,login(user1,'20.20.20.20')),
sendMsg(XID,user2,0,request,login(user2,'40.40.40.40')).
switch_thread() :-
sendMsgSync(XID,task,0,switch,[]),
rcvMsg(XID,task,From,switch,[]).