362 lines
8.3 KiB
Perl
362 lines
8.3 KiB
Perl
|
/*
|
||
|
|
|
||
|
|
CEM
|
||
|
|
|
||
|
|
Copyright (c) 2011, Fabrizio Riguzzi
|
||
|
|
|
||
|
|
*/
|
||
|
|
|
||
|
|
:- module(inference,[find_deriv_inf1/3]).
|
||
|
|
|
||
|
|
|
||
|
|
:-multifile setting/2.
|
||
|
|
:-dynamic setting/2.
|
||
|
|
|
||
|
|
%:-load_foreign_files(['cplint'],[],init_my_predicates).
|
||
|
|
|
||
|
|
|
||
|
|
:-use_module(library(lists)).
|
||
|
|
:-use_module(library(avl)).
|
||
|
|
|
||
|
|
/* start of list of parameters that can be set by the user with
|
||
|
|
set(Parameter,Value) */
|
||
|
|
setting(epsilon_parsing,0.00001).
|
||
|
|
setting(save_dot,false).
|
||
|
|
setting(ground_body,true).
|
||
|
|
/* available values: true, false
|
||
|
|
if true, both the head and the body of each clause will be grounded, otherwise
|
||
|
|
only the head is grounded. In the case in which the body contains variables
|
||
|
|
not appearing in the head, the body represents an existential event */
|
||
|
|
|
||
|
|
/* end of list of parameters */
|
||
|
|
|
||
|
|
/* s(GoalsLIst,Prob) compute the probability of a list of goals
|
||
|
|
GoalsLis can have variables, s returns in backtracking all the solutions with their
|
||
|
|
corresponding probability */
|
||
|
|
|
||
|
|
|
||
|
|
find_deriv_inf1(GoalsList,DB,Deriv):-
|
||
|
|
solve1(GoalsList,DB,[],Deriv).
|
||
|
|
|
||
|
|
find_deriv_inf(GoalsList,D,Deriv):-
|
||
|
|
solve(GoalsList,D,[],Deriv).
|
||
|
|
/* duplicate can appear in the C set because two different unistantiated clauses may become the
|
||
|
|
same clause when instantiated */
|
||
|
|
|
||
|
|
solve([],_D,C,C):-!.
|
||
|
|
|
||
|
|
solve([\+ H|T],DB,CIn,COut):-
|
||
|
|
functor(H,F,Args),
|
||
|
|
Args1 is Args-1,
|
||
|
|
user:input_cw(F/Args1),!,
|
||
|
|
call(user:neg(H)),
|
||
|
|
solve(T,DB,CIn,COut).
|
||
|
|
|
||
|
|
solve([\+ H |T],DB,CIn,COut):-!,
|
||
|
|
DB > 0,
|
||
|
|
DB1 is DB-1,
|
||
|
|
list2and(HL,H),
|
||
|
|
functor(H,F,Args),
|
||
|
|
Args1 is Args-1,
|
||
|
|
(user:input(F/Args1)->
|
||
|
|
call(user:neg(H))
|
||
|
|
;
|
||
|
|
\+ H
|
||
|
|
),
|
||
|
|
(setof(D,find_deriv_inf(HL,DB1,D),L)->
|
||
|
|
choose_clauses(CIn,L,C1),
|
||
|
|
solve(T,DB1,C1,COut)
|
||
|
|
;
|
||
|
|
solve(T,DB1,CIn,COut)
|
||
|
|
).
|
||
|
|
|
||
|
|
|
||
|
|
solve([H|T],D,CIn,COut):-
|
||
|
|
builtin(H),!,
|
||
|
|
call(H),
|
||
|
|
solve(T,D,CIn,COut).
|
||
|
|
|
||
|
|
solve([H|T],DB,CIn,COut):-
|
||
|
|
user:db(H),!,
|
||
|
|
call(user:H),
|
||
|
|
solve(T,DB,CIn,COut).
|
||
|
|
|
||
|
|
solve([H|T],DB,CIn,COut):-
|
||
|
|
functor(H,F,Args),
|
||
|
|
Args1 is Args-1,
|
||
|
|
user:input_cw(F/Args1),!,
|
||
|
|
call(user:H),
|
||
|
|
solve(T,DB,CIn,COut).
|
||
|
|
|
||
|
|
solve([H|T],D,CIn,COut):-
|
||
|
|
functor(H,F,Args),
|
||
|
|
Args1 is Args-1,
|
||
|
|
user:input(F/Args1),
|
||
|
|
call(user:H),
|
||
|
|
solve(T,D,CIn,COut).
|
||
|
|
|
||
|
|
solve([H|T],D,CIn,COut):-
|
||
|
|
user:def_rule(H,B),
|
||
|
|
append(B,T,NG),
|
||
|
|
solve(NG,D,CIn,COut).
|
||
|
|
|
||
|
|
solve([H|T],D,CIn,COut):-
|
||
|
|
D>=1,
|
||
|
|
find_rule(H,(R,S,N),B,CIn),
|
||
|
|
solve_pres(R,S,N,B,T,D,CIn,COut).
|
||
|
|
|
||
|
|
solve_pres(R,S,N,B,T,D,CIn,COut):-
|
||
|
|
member_eq((N,R,S),CIn),!,
|
||
|
|
append(B,T,NG),
|
||
|
|
D1 is D-1,
|
||
|
|
solve(NG,D1,CIn,COut).
|
||
|
|
|
||
|
|
solve_pres(R,S,N,B,T,D,CIn,COut):-
|
||
|
|
append(CIn,[(N,R,S)],C1),
|
||
|
|
append(B,T,NG),
|
||
|
|
D1 is D-1,
|
||
|
|
solve(NG,D1,C1,COut).
|
||
|
|
|
||
|
|
|
||
|
|
solve1([],_D,C,C):-!.
|
||
|
|
|
||
|
|
solve1([\+ H |T],DB,CIn,COut):-!,
|
||
|
|
DB>=1,
|
||
|
|
list2and(HL,H),
|
||
|
|
findall(D,find_deriv_inf1(HL,DB,D),L),
|
||
|
|
choose_clauses(CIn,L,C1),
|
||
|
|
solve(T,C1,COut).
|
||
|
|
|
||
|
|
solve1([H|T],D,CIn,COut):-
|
||
|
|
user:def_rule(H,B),
|
||
|
|
append(B,T,NG),
|
||
|
|
solve(NG,D,CIn,COut).
|
||
|
|
|
||
|
|
solve1([H|T],D,CIn,COut):-
|
||
|
|
D>=1,
|
||
|
|
find_rule(H,(R,S,N),B,CIn),
|
||
|
|
solve_pres(R,S,N,B,T,D,CIn,COut).
|
||
|
|
|
||
|
|
|
||
|
|
not_present_with_a_different_head(_N,_R,_S,[]).
|
||
|
|
|
||
|
|
not_present_with_a_different_head(N,R,S,[(N,R,S)|T]):-!,
|
||
|
|
not_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
not_present_with_a_different_head(N,R,S,[(_N1,R,S1)|T]):-
|
||
|
|
S\=S1,!,
|
||
|
|
not_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
not_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
|
||
|
|
R\=R1,
|
||
|
|
not_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
/* find_rule(G,(R,S,N),Body,C) takes a goal G and the current C set and
|
||
|
|
returns the index R of a disjunctive rule resolving with G together with
|
||
|
|
the index N of the resolving head, the substitution S and the Body of the
|
||
|
|
rule */
|
||
|
|
find_rule(H,(R,S,N),Body,C):-
|
||
|
|
user:rule(H,_P,N,R,S,_,_Head,Body),
|
||
|
|
not_already_present_with_a_different_head(N,R,S,C).
|
||
|
|
|
||
|
|
not_already_present_with_a_different_head(_N,_R,_S,[]).
|
||
|
|
|
||
|
|
not_already_present_with_a_different_head(N,R,S,[(N1,R,S1)|T]):-
|
||
|
|
not_different(N,N1,S,S1),!,
|
||
|
|
not_already_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
not_already_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
|
||
|
|
R\==R1,
|
||
|
|
not_already_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
not_different(_N,_N1,S,S1):-
|
||
|
|
S\=S1,!.
|
||
|
|
|
||
|
|
not_different(N,N1,S,S1):-
|
||
|
|
N\=N1,!,
|
||
|
|
dif(S,S1).
|
||
|
|
|
||
|
|
not_different(N,N,S,S).
|
||
|
|
|
||
|
|
|
||
|
|
member_head(H,[(H:_P)|_T],N,N).
|
||
|
|
|
||
|
|
member_head(H,[(_H:_P)|T],NIn,NOut):-
|
||
|
|
N1 is NIn+1,
|
||
|
|
member_head(H,T,N1,NOut).
|
||
|
|
|
||
|
|
/* choose_clauses(CIn,LC,COut) takes as input the current C set and
|
||
|
|
the set of C sets for a negative goal and returns a new C set that
|
||
|
|
excludes all the derivations for the negative goals */
|
||
|
|
choose_clauses(C,[],C).
|
||
|
|
|
||
|
|
choose_clauses(CIn,[D|T],COut):-
|
||
|
|
member((N,R,S),D),
|
||
|
|
already_present_with_a_different_head(N,R,S,CIn),!,
|
||
|
|
choose_a_head(N,R,S,CIn,C1),
|
||
|
|
choose_clauses(C1,T,COut).
|
||
|
|
|
||
|
|
|
||
|
|
choose_clauses(CIn,[D|T],COut):-
|
||
|
|
member((N,R,S),D),
|
||
|
|
new_head(N,R,S,N1),
|
||
|
|
\+ already_present(N1,R,S,CIn),
|
||
|
|
impose_dif_cons(R,S,CIn),
|
||
|
|
choose_clauses([(N1,R,S)|CIn],T,COut).
|
||
|
|
|
||
|
|
impose_dif_cons(_R,_S,[]):-!.
|
||
|
|
|
||
|
|
impose_dif_cons(R,S,[(_NH,R,SH)|T]):-!,
|
||
|
|
dif(S,SH),
|
||
|
|
impose_dif_cons(R,S,T).
|
||
|
|
|
||
|
|
impose_dif_cons(R,S,[_H|T]):-
|
||
|
|
impose_dif_cons(R,S,T).
|
||
|
|
|
||
|
|
/* instantiation_present_with_the_same_head(N,R,S,C)
|
||
|
|
takes rule R with substitution S and selected head N and a C set
|
||
|
|
and asserts dif constraints for all the clauses in C of which RS
|
||
|
|
is an instantitation and have the same head selected */
|
||
|
|
instantiation_present_with_the_same_head(_N,_R,_S,[]).
|
||
|
|
|
||
|
|
instantiation_present_with_the_same_head(N,R,S,[(NH,R,SH)|T]):-
|
||
|
|
\+ \+ S=SH,!,
|
||
|
|
dif_head_or_subs(N,R,S,NH,SH,T).
|
||
|
|
|
||
|
|
instantiation_present_with_the_same_head(N,R,S,[_H|T]):-
|
||
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
||
|
|
|
||
|
|
dif_head_or_subs(N,R,S,NH,_SH,T):-
|
||
|
|
dif(N,NH),
|
||
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
||
|
|
|
||
|
|
dif_head_or_subs(N,R,S,N,SH,T):-
|
||
|
|
dif(S,SH),
|
||
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
||
|
|
|
||
|
|
/* case 1 of Select: a more general rule is present in C with
|
||
|
|
a different head, instantiate it */
|
||
|
|
choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T]):-
|
||
|
|
S=SH,
|
||
|
|
dif(N,NH).
|
||
|
|
|
||
|
|
/* case 2 of Select: a more general rule is present in C with
|
||
|
|
a different head, ensure that they do not generate the same
|
||
|
|
ground clause */
|
||
|
|
choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T]):-
|
||
|
|
\+ \+ S=SH, S\==SH,
|
||
|
|
dif(N,NH),
|
||
|
|
dif(S,SH).
|
||
|
|
|
||
|
|
choose_a_head(N,R,S,[H|T],[H|T1]):-
|
||
|
|
choose_a_head(N,R,S,T,T1).
|
||
|
|
|
||
|
|
/* select a head different from N for rule R with
|
||
|
|
substitution S, return it in N1 */
|
||
|
|
new_head(N,R,S,N1):-
|
||
|
|
user:rule_by_num(R,S,Numbers,Head,_Body),
|
||
|
|
Head\=uniform(_,_,_),!,
|
||
|
|
nth0(N, Numbers, _Elem, Rest),
|
||
|
|
member(N1,Rest).
|
||
|
|
|
||
|
|
already_present_with_a_different_head(N,R,S,[(NH,R,SH)|_T]):-
|
||
|
|
\+ \+ S=SH,NH \= N.
|
||
|
|
|
||
|
|
already_present_with_a_different_head(N,R,S,[_H|T]):-
|
||
|
|
already_present_with_a_different_head(N,R,S,T).
|
||
|
|
|
||
|
|
|
||
|
|
/* checks that a rule R with head N and selection S is already
|
||
|
|
present in C (or a generalization of it is in C) */
|
||
|
|
already_present(N,R,S,[(N,R,SH)|_T]):-
|
||
|
|
S=SH.
|
||
|
|
|
||
|
|
already_present(N,R,S,[_H|T]):-
|
||
|
|
already_present(N,R,S,T).
|
||
|
|
|
||
|
|
/* rem_dup_lists removes the C sets that are a superset of
|
||
|
|
another C sets further on in the list of C sets */
|
||
|
|
/* rem_dup_lists removes the C sets that are a superset of
|
||
|
|
another C sets further on in the list of C sets */
|
||
|
|
rem_dup_lists([],L,L).
|
||
|
|
|
||
|
|
rem_dup_lists([H|T],L0,L):-
|
||
|
|
(member_subset(H,T);member_subset(H,L0)),!,
|
||
|
|
rem_dup_lists(T,L0,L).
|
||
|
|
|
||
|
|
rem_dup_lists([H|T],L0,L):-
|
||
|
|
rem_dup_lists(T,[H|L0],L).
|
||
|
|
|
||
|
|
member_subset(E,[H|_T]):-
|
||
|
|
subset_my(H,E),!.
|
||
|
|
|
||
|
|
member_subset(E,[_H|T]):-
|
||
|
|
member_subset(E,T).
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
member_eq(A,[H|_T]):-
|
||
|
|
A==H,!.
|
||
|
|
|
||
|
|
member_eq(A,[_H|T]):-
|
||
|
|
member_eq(A,T).
|
||
|
|
|
||
|
|
subset_my([],_).
|
||
|
|
|
||
|
|
subset_my([H|T],L):-
|
||
|
|
member_eq(H,L),
|
||
|
|
subset_my(T,L).
|
||
|
|
|
||
|
|
remove_duplicates_eq([],[]).
|
||
|
|
|
||
|
|
remove_duplicates_eq([H|T],T1):-
|
||
|
|
member_eq(H,T),!,
|
||
|
|
remove_duplicates_eq(T,T1).
|
||
|
|
|
||
|
|
remove_duplicates_eq([H|T],[H|T1]):-
|
||
|
|
remove_duplicates_eq(T,T1).
|
||
|
|
|
||
|
|
builtin(_A is _B).
|
||
|
|
builtin(_A > _B).
|
||
|
|
builtin(_A < _B).
|
||
|
|
builtin(_A >= _B).
|
||
|
|
builtin(_A =< _B).
|
||
|
|
builtin(_A =:= _B).
|
||
|
|
builtin(_A =\= _B).
|
||
|
|
builtin(true).
|
||
|
|
builtin(false).
|
||
|
|
builtin(_A = _B).
|
||
|
|
builtin(_A==_B).
|
||
|
|
builtin(_A\=_B).
|
||
|
|
builtin(_A\==_B).
|
||
|
|
builtin(length(_L,_N)).
|
||
|
|
builtin(member(_El,_L)).
|
||
|
|
builtin(average(_L,_Av)).
|
||
|
|
builtin(max_list(_L,_Max)).
|
||
|
|
builtin(min_list(_L,_Max)).
|
||
|
|
builtin(nth0(_,_,_)).
|
||
|
|
builtin(nth(_,_,_)).
|
||
|
|
average(L,Av):-
|
||
|
|
sum_list(L,Sum),
|
||
|
|
length(L,N),
|
||
|
|
Av is Sum/N.
|
||
|
|
|
||
|
|
list2or([],true):-!.
|
||
|
|
|
||
|
|
list2or([X],X):-
|
||
|
|
X\=;(_,_),!.
|
||
|
|
|
||
|
|
list2or([H|T],(H ; Ta)):-!,
|
||
|
|
list2or(T,Ta).
|
||
|
|
|
||
|
|
list2and([],true):-!.
|
||
|
|
|
||
|
|
list2and([X],X):-
|
||
|
|
X\=(_,_),!.
|
||
|
|
|
||
|
|
list2and([H|T],(H,Ta)):-!,
|
||
|
|
list2and(T,Ta).
|
||
|
|
|