%% proof.pl

:- use_module( library( lists ), [member/2,append/3] ).


%% The Program

rule( s, [np,vp] ).
rule( s1, [c,s] ).

rule( vp, [v] ).
rule( vp, [v,s1] ).

rule( np, [d,n] ).
rule( np, [it] ).         fact( it ).     %rule( it, [] ).
rule( np, [they] ).       fact( they ).   %rule( they, [] ).
rule( np, [them] ).       fact( them ).   %rule( them, [] ).


rule( n, [entity] ).      fact( entity ).   %rule( entity, [] ).
rule( n, [entities] ).    fact( entities ). %rule( entities, [] ).
rule( n, [thing] ).       fact( thing ).    %rule( thing, [] ).
rule( n, [things] ).      fact( things ).   %rule( things, [] ).
rule( n, [idea] ).        fact( idea ).     %rule( idea, [] ).
rule( n, [ideas] ).       fact( ideas ).    %rule( ideas, [] ).

rule( d, [a] ).           fact( a ).
rule( d, [an] ).          fact( an ).
rule( d, [the] ).         fact( the ).
rule( d, [few] ).         fact( few ).
rule( d, [most] ).        fact( most ).
rule( d, [every] ).       fact( every ).
rule( d, [some] ).        fact( some ).

rule( v, [exists] ).      fact( exists ).
rule( v, [exist] ).       fact( exist ).
rule( v, [thinks] ).      fact( thinks ).
rule( v, [think] ).       fact( think ).
rule( v, [wonder] ).      fact( wonder ).
rule( v, [wonders] ).     fact( wonders ).

rule( c, [that] ).        fact( that ).
rule( c, [if] ).          fact( if ).









%% Several Interpreters


%% 1. Proplog interpreter

prove( [] ).
prove( [Goal|OldGoals] ):-
	fact( Goal ),
	prove( OldGoals ).
prove( [Goal|OldGoals] ):-
	rule( Goal, NewGoals ),
	prove( NewGoals ),
	prove( OldGoals ).


%% 2. Proving "sequents": Facts derive Goals

derive( [], [] ).
derive( Facts, [Goal|OtherGoals] ):-
	fact( Goal ),
	Facts = [Goal|OtherFacts],
	derive( OtherFacts, OtherGoals ).
derive( Facts, [Goal|OldGoals] ):-
	rule( Goal, NewGoals ),
	append( TheseFacts, ThoseFacts, Facts ),
	derive( TheseFacts, NewGoals ),
	derive( ThoseFacts, OldGoals ).


%% 3. Constructing proof trees: A proof of Goals is Proof

proof( [], [] ).
proof( [Goal|OldGoals], Proof ):-
	fact( Goal ),
	proof( OldGoals, PfOldGoals ),
	Proof = [ -(Goal) | PfOldGoals ].
proof( [Goal|OldGoals], Proof ):-
	rule( Goal, NewGoals ),
	proof( NewGoals, PfNewGoals ),
	proof( OldGoals, PfOldGoals ),
	Proof = [ Goal/PfNewGoals | PfOldGoals ].


%% For comparison:

forest( [] ).
forest( [T|Ts] ):-
	terminal( T ),
	forest( Ts ).
forest( [T|Ts] ):-
	nonterminal( T, Subtrees ),
	forest( Subtrees ),
	forest( Ts ).

terminal( -_ ).

nonterminal( _/Subs, Subs ).

tree( T ):- forest( [T] ).
