23:- module( tableaux, [prove/5,
24 yadlr_concept/2, yadlr_relation/2, yadlr_instance/2,
25 yadlr_concept_name/2, yadlr_relation_name/2,
26 yadlr_instance_name/2,
27 yadlr_assert/3, yadlr_init/1,
28 yadlr_retrieve_concept/2, yadlr_retrieve_instance/2,
29 set_debug_msgs/1, set_depth_limit/1,
30 set_proof_tree_log/1, unset_proof_tree_log/0] ). 31
32
33:- use_module(library(lists), [append/3,flatten/2]).
40:-
43 op(400, fy, -), 44 op(500, xfy, &), 45 op(600, xfy, v), 46 op(650, xfy, =>), 47 op(700, xfy, <=>).
56
57poslit( pred(pos,_,_,_) ). poslit( pred(pos,_,_) ).
58neglit( pred(neg,_,_,_) ). neglit( pred(neg,_,_) ).
59
60contradict( pred(pos,F,A), pred(neg,F,A) ).
61contradict( pred(neg,F,A), pred(pos,F,A) ).
62contradict( pred(pos,F,A1,A2), pred(neg,F,A1,A2) ).
63contradict( pred(neg,F,A1,A2), pred(pos,F,A1,A2) ).
75
82
83get_next( branch(Ground,Exists,Rest,[SubF|TODO]), SubF,
84 branch(Ground,Exists,[SubF|Rest],TODO) ).
85
86add_next(_, [], _) :- !, fail.
87add_next( branch(Ground1,Exists,Rest,TODO1), L, branch(Ground2,Exists,Rest,TODO2) ) :-
88 !,
89 ground_literals(L, Ground, NotGround),
90 append(Ground,Ground1,Ground2),
91 append(NotGround,TODO1,TODO2).
92
93ground_literal(p, pred(pos,p) ).
94ground_literal(q, pred(pos,q) ).
95ground_literal(-p, pred(neg,p) ).
96ground_literal(-q, pred(neg,q) ).
97
98ground_literals([], [], []).
99ground_literals([Head|Tail], Ground, Rest) :-
100 ground_literals(Tail, Ground1, Rest1),
101 (ground_literal(Head,Pred) ->
102 Ground = [Pred|Ground1], Rest = Rest1
103 ;
104 Ground = Ground1, Rest = [Head|Rest1]
105 ).
106
107expand(-(T1 <=> T2), [-(T1 => T2)], [-(T2 => T1)] ) :- !.
108expand( (T1 <=> T2), [(T1 => T2),(T2 => T1)], [] ) :- !.
109expand(-(T1 => T2), [T1,-T2], [] ) :- !.
110expand( (T1 => T2), [-T1], [T2] ) :- !.
111expand(-(T1 & T2), [-T1], [-T2]) :- !.
112expand( (T1 & T2), [T1,T2], [] ) :- !.
113expand(-(T1 v T2), [(-T1),(-T2)], []) :- !.
114expand( (T1 v T2), [T1], [T2] ) :- !.
115expand( -T, [-T], [] ) :- !.
116expand( T, [T], [] ).
117
118
125
126try_one(F,_,F).
127try_one(_,F,F).
128
129recurse( branch(Ground, Exist, Rest, []), [] ) :- !,
130 131 print(branch(Ground, Exist, Rest, [])), nl,
132 print(closed), nl,
133 fail.
134recurse(Branch, Res) :-
135 136 print(Branch), nl,
137 get_next(Branch, SubF, Branch1),
138 expand(SubF, F1, F2),
139 !,
140 try_one(F1, F2, F),
141 add_next(Branch1, F, Branch2),
142 recurse(Branch2, Res).
143
144prove(F,Res) :- recurse( branch([],[],[],[-F]), Res1 ) -> Res=Res1 ; Res=valid