%% fuzzy ALC reasoning %% using resolution as inference operator %% %% Author: Stasinos Konstantopoulos %% Created: 6-2-2007 %% Copyright (C) 2007 Stasinos Konstantopoulos %% %% This program is free software; you can redistribute it and/or modify %% it under the terms of the GNU General Public License as published by %% the Free Software Foundation; either version 2 of the License, or %% (at your option) any later version. %% %% This program is distributed in the hope that it will be useful, %% but WITHOUT ANY WARRANTY; without even the implied warranty of %% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the %% GNU General Public License for more details. %% %% You should have received a copy of the GNU General Public License along %% with this program; if not, write to the Free Software Foundation, Inc., %% 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. :- module( resolution, [prove/5, yadlr_concept/2, yadlr_relation/2, yadlr_instance/2, yadlr_concept_name/2, yadlr_relation_name/2, yadlr_instance_name/2, yadlr_assert/3, yadlr_init/1, retractKB/1, yadlr_retrieve_concept/2, yadlr_retrieve_instance/2, set_debug_msgs/1, set_depth_limit/1, set_proof_tree_log/1, unset_proof_tree_log/0] ). :- user:use_algebra( AlgModule ), use_module( AlgModule ). %% %% SETTINGS %% :- dynamic use_debug_msgs/1, use_proof_tree_log/1, use_depth_limit/1. use_debug_msgs( no ). set_debug_msgs( yes ) :- retractall( use_debug_msgs(_) ), assert_if_new( use_debug_msgs(yes) ). set_debug_msgs( no ) :- retractall( use_debug_msgs(_) ), assert_if_new( use_debug_msgs(no) ). msg_debug( Msg ) :- use_debug_msgs( yes ), fmt( '~q~n', Msg ), !. msg_debug( _ ) :- use_debug_msgs( no ), !. use_proof_tree_log( no ). set_proof_tree_log( no ) :- !, retractall( use_proof_tree_log(_) ), assert_if_new( use_proof_tree_log(no) ). set_proof_tree_log( yes ) :- !, retractall( use_proof_tree_log(_) ), assert_if_new( use_proof_tree_log(yes) ), open( 'resolution.log', write,Stream, [type(text)] ), % ,alias(yadlr_logfile) asserta(yadlr_logfile(Stream)). set_proof_tree_log( File ) :- retractall( use_proof_tree_log(_) ), assert_if_new( use_proof_tree_log(yes) ), open( File, write, Stream, [type(text)] ), % ,alias(yadlr_logfile) asserta(yadlr_logfile(Stream)). unset_proof_tree_log :- set_proof_tree_log( no ), yadlr_logfile(Stream), close( Stream ). msg_proof_tree( Depth, StepType, OpenList, RestrVars ) :- use_proof_tree_log( yes ), yadlr_format_clauses( OpenList, Clauses ), fmt_range( RestrVars, Restr ), fmt( yadlr_logfile, 'derivation(~d, ~q, ~q, ~q).~n', [Depth, StepType, Restr, Clauses] ), !. msg_proof_tree( _, _, _, _ ) :- use_proof_tree_log( no ), !. use_depth_limit( no ). set_depth_limit( N ) :- integer( N ), retractall( use_depth_limit(_) ), assert_if_new( use_depth_limit(N) ). set_depth_limit( no ) :- retractall( use_depth_limit(_) ), assert_if_new( use_depth_limit(no) ). %% %% REPRESENTATION %% % Literals are ylit(Polarity,Symbol) terms yadlr_is_literal( ylit(pos, _) ). yadlr_is_literal( ylit(neg, _) ). yadlr_mk_literal( ylit(P,S), P, S ). yadlr_mk_literals( [], _, [] ). yadlr_mk_literals( [ylit(P,Head)|Rest1], P, [Head|Rest2] ) :- yadlr_mk_literals( Rest1, P, Rest2 ). yadlr_lit_complement( ylit(pos,L), ylit(neg,L) ). yadlr_lit_complement( ylit(neg,L), ylit(pos,L) ). yadlr_lit_list_complement( [], [] ). yadlr_lit_list_complement( [H|Rest], [NotH|NotRest] ) :- yadlr_lit_complement( H, NotH ), yadlr_lit_list_complement( Rest, NotRest ). % Clauses are (Pos,Neg,Degree) tuples. % Pos and Neg are sets of literals % The abstract clause is the disjunction of union(Pos,Neg) % Degree is the fuzzy degree yadlr_mk_clause( [], Range, yclause([],[],Range) ). yadlr_mk_clause( [ylit(pos,L)|Rest], Range, yclause([ylit(pos,L)|RestPos], Neg, Range) ) :- yadlr_mk_clause( Rest, Range, yclause(RestPos,Neg,Range) ). yadlr_mk_clause( [ylit(neg,L)|Rest], Range, yclause(Pos, [ylit(neg,L)|RestNeg], Range) ) :- yadlr_mk_clause( Rest, Range, yclause(Pos,RestNeg,Range) ). yadlr_clause_pos( yclause(Pos,_,_), Pos ). yadlr_clause_neg( yclause(_,Neg,_), Neg ). yadlr_clause_degree( yclause(_,_,Degree), Degree ). yadlr_format_clauses( [], [] ). yadlr_format_clauses( [yclause(Pos,Neg,Deg)|RestIn], [yclause(Pos,Neg,FmtDeg)|RestOut] ) :- fmt_range( [Deg], FmtDeg ), yadlr_format_clauses( RestIn, RestOut ). % The KB is yadlr_kb( Clause ) terms. % TODO1: yadlr_kb( head, clause ) terms. head is redundant, but % helps the prolog engine's index mechanism. % TODO2: store the original abstract form, for log presentation % init kb: cleans KB and asserts built-in relations yadlr_init( KB ) :- retractKB( KB ), % declare reserved symbols yadlr_concept( KB, dlalldifferent ). % place grounds facts at the top yadlr_assert_one( KB, Clause ) :- yadlr_clause_neg( Clause, [] ), !, db_recorda( KB, Clause, _ ). yadlr_assert_one( KB, Clause ) :- db_recordz( KB, Clause, _ ). yadlr_assert_many( _, [] ). yadlr_assert_many( KB, [Head|Rest] ) :- yadlr_assert_one( KB, Head ), yadlr_assert_many( KB, Rest ). % TODO: check if it already exists, and fail yadlr_concept( KB, ConceptName ) :- db_recordz( KB, yconcept(ConceptName), _ ). yadlr_relation( KB, RelationName ) :- db_recordz( KB, yrelation(RelationName), _ ). yadlr_instance( KB, InstanceName ) :- db_recordz( KB, yinstance(InstanceName), _ ). yadlr_concept_name( KB, ConceptName ) :- db_recorded( KB, yconcept(ConceptName), _ ). yadlr_relation_name( KB, RelationName ) :- db_recorded( KB, yrelation(RelationName), _ ). yadlr_instance_name( KB, InstanceName ) :- db_recorded( KB, yinstance(InstanceName), _ ). yadlr_assert( KB, Formula, FuzzyDegree ) :- clausify_abstract( Formula, FuzzyDegree, Clauses ), yadlr_assert_many( KB, Clauses ). % SWI Prolog does not have eraseall/1 retractKB( KB ) :- prolog_engine(swi), db_recorded( KB, _, Ref ), erase( Ref ), fail. retractKB( _ ) :- prolog_engine(swi), !. % SWI Prolog does not have eraseall/1 % retractKB( KB ) :- eraseall( KB ). yadlr_retrieve_concept( KB, ConceptName ) :- db_recorded( KB, yconcept(ConceptName), _ ). yadlr_retrieve_relation( KB, RelationName ) :- db_recorded( KB, yrelation(RelationName), _ ). yadlr_retrieve_instance( KB, InstanceName ) :- db_recorded( KB, yinstance(InstanceName), _ ). yadlr_retrieve_clause( KB, yclause(Pos,Neg,Deg) ) :- db_recorded( KB, yclause(Pos,Neg,Deg), _ ). %% %% UTILITIES %% :- use_module( [library(lists),nfsdl] ). % SWI Prolog does not have remove_duplicates/2 % also consider file_search_path(swi, _) as a test, % as the Prolog interpreter might have been renamed /* :- ( prolog_engine(swi) -> assert_if_new( remove_duplicates([], []) ), assert_if_new( (remove_duplicates([Elem|L], [Elem|NL]) :- delete(L, Elem, Temp), remove_duplicates(Temp, NL)) ) ; true ). */ complement_member( L1, [L2|_]) :- yadlr_lit_complement( L1, L2 ). complement_member(Element, [_|Rest]) :- complement_member(Element, Rest). % complement_intersection/5 (+List1, +List2, ?Intersection1, -Rest1, -Rest2) complement_intersection( [], _, [], _, _ ). complement_intersection( [H|T], L2, [H|I], T, Rest2 ) :- complement_member( H, L2 ), !, yadlr_lit_complement( H, NotH ), complement_intersection( T, L2, I, T, R2 ), select( NotH, R2, Rest2 ). complement_intersection( [H|T], L2, I, [H|R1], R2 ) :- complement_intersection( T, L2, I, R1, R2 ). % straight_intersection/5 (+List1, +List2, ?Intersection, -Rest1, -Rest2) straight_intersection( [], L2, [], [], L2 ). straight_intersection( [H|T], L2, [H|I], T, Rest2 ) :- member( H, L2 ), !, straight_intersection( T, L2, I, T, R2 ), select( H, R2, Rest2 ). straight_intersection( [H|T], L2, I, [H|R1], R2 ) :- straight_intersection( T, L2, I, R1, R2 ). % C1 is a subset of C2, and C1 is more certain fuzzy_subsumes( Clause1, Clause2, Residue ) :- yadlr_clause_degree( Clause1, D1 ), yadlr_clause_degree( Clause2, D2 ), less_fuzzy( D1, D2 ), yadlr_clause_pos( Clause1, Pos1 ), yadlr_clause_pos( Clause2, Pos2 ), permutation( Pos1, P1 ), append( P1, PosRes, Pos2 ), yadlr_clause_neg( Clause1, Neg1 ), yadlr_clause_neg( Clause2, Neg2 ), permutation( Neg1, N1 ), append( N1, NegRes, Neg2 ), append( PosRes, NegRes, Residue ). % clausify_literals( ?[Literals], ?Degree, ?[Clauses] ) % % turns a list of literals into a list of single-literal clauses % all clauses have fuzzy degree Degree clausify_literals( [], _, []). clausify_literals( [L|RestL], Degree, [C|RestC] ) :- yadlr_mk_clause( [L], Degree, C ), clausify_literals( RestL, Degree, RestC ). % clausify_abstract( +Formula, +FuzzyDegree, -[YClauses] ) % % turns an abstract formula into a list of yclauses clausify_abstract( Formula, FuzzyDegree, Clauses ) :- is_fuzzy_degree( FuzzyDegree ), nnf( Formula, NNF ), pnf( NNF, PNF ), cf( PNF, CF ), cf_to_yclauses( CF, FuzzyDegree, Clauses ). cf_to_yclauses( [], _, [] ). cf_to_yclauses( [CF|T1], FuzzyDegree, [Clause|T2] ) :- cf_to_yclause( CF, FuzzyDegree, Clause ), cf_to_yclauses( T1, FuzzyDegree, T2 ). cf_to_yclause( cl(Pos,Neg), FuzzyDegree, Clause ) :- yadlr_mk_literals( PosLits, pos, Pos ), yadlr_mk_literals( NegLits, neg, Neg ), append( PosLits, NegLits, Lits ), yadlr_mk_clause( Lits, FuzzyDegree, Clause ). %% %% RESOLUTION %% % Clause1-Clause2 are instantiated and complement-intersect % % NOTE: implementation guarantees that Clause1 is the one providing % the pos literals. This is needed for fuzzy degree checking, % do not attempt neg(Clause1)-pos(Clause2). compatible( Clause1, Clause2, Inters, Residue ) :- var( Inters ), !, yadlr_clause_pos( Clause1, Pos ), yadlr_clause_neg( Clause2, Neg ), complement_intersection( Pos, Neg, Inters, Rest1, Rest2 ), append( Rest1, Rest2, Residue ). % Clause1-Inters are instantiated and Inters is a subset of Clause1 % TODO: do not require Inters subset Clause1, to get non-definite resolution compatible( Clause1, Clause2, Inters, Residue ) :- var( Clause2 ), !, yadlr_mk_clause( LitList1, _, Clause1 ), yadlr_mk_clause( LitListI, _, Inters ), straight_intersection( LitList1, LitListI, LitListI, R, [] ), yadlr_lit_list_complement( R, NotR ), % union(LitList2,Residue) must be NotR permutation( NotR, A ), append( LitList2, Residue, A ), % make a half-baked Clause2 yadlr_mk_clause( LitList2, _, Clause2 ). resolve( Clause1, Clause2, Res, RestrVarsIn, RestrVarsOut ) :- nonvar( Clause1 ), nonvar( Clause2 ), var( Res ), !, % look for the complement-intersection of Clause1 % and Clause2. compatible( Clause1, Clause2, _Inters, Residue ), % check degrees yadlr_clause_degree( Clause1, Deg1 ), yadlr_clause_degree( Clause2, Deg2 ), less_fuzzy( Deg2, Deg1 ), % calculate degree range for Res clause tnorm( mp, Deg1, Deg2, DegR ), yadlr_mk_clause( Residue, DegR, Res ), (var(Deg1) -> append([Deg1], RestrVarsIn, RestrVars1) ; RestrVars1 = RestrVarsIn), (var(Deg2) -> append([Deg2], RestrVars1, RestrVarsOut) ; RestrVarsOut = RestrVars1). resolve( Clause1, Clause2, Res, RestrVarsIn, RestrVarsOut ) :- nonvar( Clause1 ), var( Clause2 ), nonvar( Res ), !, % Theorize about Clause2: Residue gets unified with % what needs to be proven to prove Res. % Clause2 gets unified with the perfect clause that % would do the job without any residue. compatible( Clause1, Clause2, Res, [] ), % check degrees yadlr_clause_degree( Clause1, Deg1 ), yadlr_clause_degree( Res, DegR ), less_fuzzy( Deg1, DegR ), tnorm( mp, Deg1, Deg2, DegR ), yadlr_clause_degree( Clause2, Deg2 ), (var(Deg1) -> append([Deg1], RestrVarsIn, RestrVarsOut) ; RestrVarsIn = RestrVarsOut ). % resolution_step( +KB, +Clause, -OpenList ) % perform a single resolution step resolution_step( KB, Clause, ResidualClauses, RestrIn, RestrOut ) :- yadlr_retrieve_clause( KB, Clause1 ), resolve( Clause1, Residue, Clause, RestrIn, RestrOut ), % Residue is a pos-only clause that remains to be % proven; turn into a list of atomic clauses yadlr_mk_clause( Literals, Degree, Residue ), % The fuzzy degree of the clause will be the % fuzzy degree of each clausified literal clausify_literals( Literals, Degree, ResidualClauses ). tautology_check( [Clause|RestIn], RestOut ) :- % if a literal appears as both pos and neg, % then the clause is a tautology yadlr_clause_pos( Clause, Pos ), yadlr_clause_neg( Clause, Neg ), \+ complement_intersection( Pos, Neg, [], _, _ ), !, tautology_check( RestIn, RestOut ). tautology_check( [Clause|RestIn], [Clause|RestOut] ) :- tautology_check( RestIn, RestOut ). %% %% makealldiff/1 ( +List ) %% ensures that all elements of are ununifiable %% checkalldiffhelper( _, [] ). checkalldiffhelper( A, [B] ) :- A \= B. checkalldiffhelper( A, [H|R] ) :- A \= H, checkalldiffhelper( A, R ). checkalldiff( [] ). checkalldiff( [_] ). checkalldiff( [H|R] ) :- checkalldiffhelper( H, R ), checkalldiff( R ). has_vars( [H] ) :- var( H ). has_vars( [H|R] ) :- var( H ) ; has_vars( R ). %% %% lr_pass/7 ( +KB, +Depth, +Clauses, +OpenListIn, -OpenListOut, +RestrVarsIn, -RestrVarsOut ) %% % if the restrictions narrow Degree down to zero, the branch % is done for lr_pass( _, Depth, _, Open, Open, RestrVars, RestrVars ) :- check_clause_degree( RestrVars, 0.0 ), NewDepth is Depth + 1, msg_proof_tree( NewDepth, f, Open, _RestrVarsIn ). % nothing left to prove, success lr_pass( _, Depth, [], Open, Open, RestrVars, RestrVars ) :- NewDepth is Depth + 1, msg_proof_tree( NewDepth, t, Open, RestrVars ). % complement lr_pass( KB, Depth, [H|Rest], OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ) :- yadlr_clause_neg( H, [NegLit] ), NewDepth is Depth + 1, yadlr_mk_literal( NegLit, neg, Lit ), yadlr_clause_degree( H, OldDegree ), tnorm( complement, OldDegree, NewDegree ), yadlr_mk_literal( PosLit, pos, Lit ), yadlr_mk_clause( [PosLit], NewDegree, Clause ), once( msg_proof_tree(NewDepth,compl,[Clause|Rest],RestrVarsIn) ), lr_pass( KB, NewDepth, [Clause|Rest], OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ). % defer uninstantiated dlalldifferent/1 literals lr_pass( KB, Depth, [H|Rest], OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ) :- yadlr_clause_pos( H, [Lit] ), yadlr_mk_literal( Lit, pos, dlalldifferent(DiffList) ), has_vars( DiffList ), NewDepth is Depth + 1, append( Rest, [H], NewRest ), once( msg_proof_tree(NewDepth, sp, NewRest, RestrVarsIn) ), lr_pass( KB, NewDepth, NewRest, OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ). % check instantiated dlalldifferent/1 literals lr_pass( KB, Depth, [H|Rest], OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ) :- yadlr_clause_pos( H, [Lit] ), yadlr_mk_literal( Lit, pos, dlalldifferent(DiffList) ), \+ has_vars( DiffList ), NewDepth is Depth + 1, once( msg_proof_tree(NewDepth, sp, [H|Rest], RestrVarsIn) ), checkalldiff( DiffList ), lr_pass( KB, NewDepth, Rest, OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ). % apply resolution step lr_pass( KB, Depth, [H|Rest], OpenIn, OpenOut, RestrVarsIn, RestrVarsOut ) :- NewDepth is Depth + 1, resolution_step( KB, H, ResidualClauses, RestrVarsIn, RestrVars1 ), append( Rest, ResidualClauses, NewRest1 ), remove_duplicates( NewRest1, NewRest ), once( msg_proof_tree(NewDepth, mp, NewRest, RestrVars1) ), lr_pass( KB, NewDepth, NewRest, OpenIn, OpenOut, RestrVars1, RestrVarsOut ), append( [H|Rest], OpenIn, _ToDo ). %msg_proof_tree( NewDepth, mp, ToDo ). lr_pass( KB, Depth, [H|Rest], OpenIn, [H|OpenList], RestrVarsIn, RestrVarsOut ) :- NewDepth is Depth + 1, lr_pass( KB, NewDepth, Rest, [H|OpenIn], OpenList, RestrVarsIn, RestrVarsOut ), append( Rest, [H|OpenIn], ToDo ), msg_proof_tree( NewDepth, s, ToDo, RestrVarsOut ). prove_clauses( KB, Depth, Clauses, Open, RestrVarsIn, RestrVarsOut ) :- msg_proof_tree( 0, i, Clauses, RestrVarsIn ), lr_pass( KB, Depth, Clauses, [], Open, RestrVarsIn, RestrVarsOut ). %% prove/5 ( +KB, +Query, ?FuzzyDegree, -Open, -ExtraRestr ) prove( KB, Query, FuzzyDegree, Open, Restr ) :- var(FuzzyDegree), !, clausify_abstract( Query, FuzzyDegree, Clauses ), prove_clauses( KB, 0, Clauses, Open, [FuzzyDegree], RestrVars ), fmt_range( RestrVars, Restr ), % if FuzzyDegree has not been instantiated, % set to max allowed by restrictions % this is only possible if all inputs are instantiated % (ie, there only one element, d, in RestrVars) (var(FuzzyDegree), length( RestrVars, 1 ) -> nth0( 0, RestrVars, Deg ), get_max(Deg,FuzzyDegree) ; true ). prove( KB, Query, FuzzyDegree, Open, Restr ) :- float(FuzzyDegree), !, clausify_abstract( Query, Degree, Clauses ), less_fuzzy( Degree, FuzzyDegree ), prove_clauses( KB, 0, Clauses, Open, [Degree], RestrVars ), fmt_range( RestrVars, Restr ).