/* $Id: rdfpf.pl,v 1.1 2001/09/06 21:12:54 connolly Exp $
 * check a proof based on the cwm logic.
 *
 * Maybe cwm logic is pretty much just FOPL, in which
 * case pretty normal model theory/proof theory applies,
 * where quantifiers apply to terms;
 * in this case log:forAll and log:forSome are *not* normal
 * triples.
 *
 * But on the other hand, maybe they can be seen as normal
 * triples, if we take a possible-worlds approach (where
 * formulas denote sets of satisfying interpretations) and
 * apply quantifiers to objects in the domain.
 *
 * e.g. F* ::= (implies (type d Dog) (has d Fleas))
 * denotes the set ~P \U Q where
 * P is the set of interpretations that satisfy (type d Dog)
 * and Q is the set of interpretations satisfying (has d Fleas).
 * Then (forall (d) (implies (type d Dog) (has d Fleas)))
 * denotes the set { I : I \in ~P \U Q /\ I[x/d] satsfies F* forall x }, where
 * I[x/d] is an interpretation like I except that
 * where I[E] = d, I[x/d] = x.
 */

/* abstract syntax:
 * term ::= symbol | string
 * prop ::= holds(term, term, term)
 * formula ::= desc(Vars, Props)
 *     ala (exists (vars...) (and props...))
 * Vars is list of term
 * Props is list of prop
 */

/* query: check a proof that...
 * all dogs have fleas.
 * fido is a dog.
 * => fido has fleas
 */
proves(given1,
       desc([xF, xCs, xImp, xAnt, xAntCs, xAnt1, xConc],
	    [holds(log_forAll, xF, ex_x),
	     holds(log_forSome, xF, ont_nil),
	     holds(log_conjuncts, xF, xCs),
	     holds(ont_first, xCs, xImp),
	     holds(ont_rest, xCs, ont_nil),
	     holds(rdf_predicate, xImp, log_implies),
	     holds(rdf_subject, xImp, xAnt),
	     holds(rdf_object, xImp, xConc),
	     holds(log_forSome, xAnt, ont_nil),
	     holds(log_conjuncts, xAnt, xAntCs),
	     holds(ont_first, xAntCs, xAnt1),
	     holds(ont_rest, xAntCs, ont_nil),
	     holds(rdf_predicate, xAnt1, rdf_type),
	     holds(rdf_subject, xAnt1, ex_x),
	     holds(rdf_object, xAnt1, ex_Dog),

		       desc([],
			    [holds(log_implies,
			      desc([], holds(rdf_type, ex_x, ex_Dog)),
			      desc([], holds(ex_has, ex_x, ex_Fleas)))]),
		       x)] )).
proves(given2, desc([], [holds(rdf_type, ex_fido, ex_Dog)])).

/* query: proves(Pf, desc([], [holds(ex_has, ex_fido, ex_Fleas)])) */


/* Rx1: andE (aka erasure).
   Hmm... the scope of an anonymous subject in RDF is *not*
   the whole file: from
          :book1 :title "xyz".
          :fred :friend [ :hairColor "brown" ].
   I should be able to deduce
          :book1 :title "xyz".
   hmm... or is it... i.e. is it sound to
   deduce A from (exists (?x) A) where ?x does not occur in A?
   presuming the universe of discourse is not empty, I suppose it is sound.
 */
proves(andE(MorePf), desc(VarsOut, Fewer)) :-
  subset(Fewer, More),
  termsUsed(Fewer, T),
  intersection(VarsIn, T, VarsOut),
  proves(MorePf, desc(VarsIn, More)).

termsUsed(desc(_, []), []).
termsUsed(desc(Vars, [holds(P, S, O) | Rest]), T) :-
  terms(desc(Vars, Rest), Trest),
  list_to_set([P, S, O], Tpso),
  merge_set(Tpso, Trest, T).


 /* subset/2 is part of the swi-prolog library
    file:/usr/share/doc/swi-prolog/html/sec-3.30.html
    in a debian install of swi-prolog
  */


/* Rx2: andI.
 * (=> (and (exist (?x ?y ?z ...) (and ...A...))
 *          (exist (?p ?q ?r ...) (and ...B...)))
 *     (exist (?x ?y ?z ... ?p ?q ?r) (and ...A... ...B...)) )
 */
proves(andI(Apf, Bpf), desc(VarsAuB, AuB) :-
  union(A, B, AuB),
  union(VarsA, VarsB, VarsAuB),
  intersection(VarsA, VarsB, []),
  proves(Apf, desc(VarsA, A)),
  proves(Bpf, desc(VarsB, B)).

/* union/3 and intersection/3 are part of the swi-prolog library
file:/usr/share/doc/swi-prolog/html/sec-3.30.html
*/

/* Rx3 exI:
 * from (exists (...Vars...) (...Props...))
 * conclude (exists (...V Vars...) (...Props...))
 * where V is a term from Props not in Vars.
 */
proves(exI(Ppf, V), desc(OneMoreVar, Props)) :-
	/* check symbol(V)??? */
        proves(Ppf, desc(Vars, Props)),
        termsUsed(Props, T),
	member(V, T),
	intersection([V], Vars, []),
        merge_set([V], Vars, OneMoreVar).


/* ************** */

/* Rcwm1 log_implies */
proves(mp(Ppf, PthenQpf), Q) :-
	proves(PthenQpf, desc([], [holds(log_implies, P, Q)])),
	proves(Ppf, P).


/* Rcwm2 log_forAll:
 * from (exists () (and (log_forAll F V)
                        (log_forSome F @@@@
 */
proves(uexp(AllPf, Uvar, Term), desc(ExVars, SpeclProps)) :-
	subst(Uvar, Term, GenlProps, SpeclProps),
	intersection([Uvar], ExVars, []),
	proves(AllPf,
               desc([], [holds(log_forAll, F, Uvar)])),
        proves(PfReifyF
desc(ExVars, GenlProps)


subst(_, _, [], []).
subst(Var, Term, [holds(P, S, O) | Rest ],
                 [holds(PP, SS, OO) | RestAfter]) :-
	sub1(Var, Term, P, PP),
	sub1(Var, Term, S, SS),
	sub1(Var, Term, O, OO),
	subst(Var, Term, Rest, RestAfter).

sub1(Var, Term, Var, Term).
sub1(_, _, Other, Other). /* relies on NAF */

/*  RsNN log_Truth
*
*proves(truth(Ppf), desc([], holds(P, S, O))) :-
*  proves(Ppf, desc([], holds(rdf_type, reify(P, S, O), log_Truth)).
*/