# Prolog Forward Chaining LogicMOO is an extension of Prolog that is complete for the full first­order predicate calculus (Stickel, 1988). It is invoked whenever the facts and rule are described in PNF, NNF or CNF into the knowledge base. However, when the rules are in Prenix Normal Form (PNF) (thus have quantifiers) they are converted to NNF, SNF and finally CNF and handed back over to WFS. Whenever a formula whose leading quantifier is existential occurs, the formula obtained by removing that quantifier via Skolemization may be generated. LogicMOO is an Dynamic Epistemic Logic is the logic of knowledge and belief. LogicMOO uses a non-monotonic logic (a formal logic whose consequence relation is not monotonic). In other words, it is devised to capture and represent defeasible inferences (c.f. defeasible reasoning), i.e., a kind of inference in which reasoners draw tentative conclusions, enabling reasoners to retract their conclusion(s) based on further evidence. In contrast, most studied formal logics have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences. Monotonicity indicates that learning a new piece of knowledge cannot reduce the set of what is known. A monotonic logic cannot handle various reasoning tasks such as reasoning by default (consequences may be derived only because of lack of evidence of the contrary), abductive reasoning (consequences are only deduced as most likely explanations), some important approaches to reasoning about knowledge (the ignorance of a consequence must be retracted when the consequence becomes known), and similarly, belief revision (new knowledge may contradict old beliefs). Negation by failure (only in rare cases): I might infer that I do not have a sister, since, if I did, I would certainly know it, and I do not in fact know that I have a sister. Such an inference is, of course, defeasible, since if I subsequently learn that I have a sister after all, the basis for the original inference is nullified. Thus, the system *changes* what is beleived to be factual as time goes on. Ideally the system's beliefs are revised in such a way that when new information is aquired the knowledge will remnain consistant. This is why LogicMOO has to power to be considered a Dynamic Epistemic Logic system. This lesson will show how this is done This skeleton notebook pre-loads SWI-Prolog's libraries for Dynamic Epistemic Logic (DEL) programming. The libraries are: - library(logicmoo_user) loads the framework. - library(logicmoo_base) provides DEL Logic. - library(logicmoo_repl) provides Toplevel Interaction. - library(logicmoo_clif) Common Logic Interchange Format. [Documentation](http://www.swi-prolog.org/pldoc/doc_for?object=clif/1) - library(logicmoo_sumo) Load the Upper logical axioms.
/* LogicMOO in operation : In this section we provide a trace of LogicMOO in operation. Input from the user follows the standard Prolog prompt (?­) or the LogicMOO prompt (?->); all other text is output from LogicMOO. LogicMOO's responses to the questions that are asked illustrate the system's reasoning capabil­ ities, and demonstrate its ability to derive the beliefs listed that summarizes the results of our data analysis. Comments are inserted with "%=" at the begginning and "reprinted". We start by sending all axioms to the PTTP compiler, which, in turn, transforms them and prints them out. */
:- use_module(library(logicmoo_user)). %= save compiled clauses using forward chaining storage (by default) %= we are using forward chaining just so any logical errors, performance and program bugs manefest %= immediately :- set_clause_compile(fwc). %= setup pfc :- file_begin(pfc). %= Trace execution :- mpred_trace_exec. (ptSymmetric(Pred) ==> ({atom(Pred),G1=..[Pred,X,Y],G2=..[Pred,Y,X]}, (G1==>G2), (neg(G1)==> neg(G2)))). % (isa(Pred, ptSymmetric)==> ((neg(t(Pred, X, Y))==>neg(t(Pred, Y, X))))). %= ```` %= logic tests... %= ```` mpred_prop(otherGender,2,prologBuiltin). otherGender(male,female). otherGender(female,male). bore_offspring(X,Y) <=> bore_offspring(Y,X). (bore_offspring(X,Y),gender(X,G1), otherGender(G1,G2)) => gender(Y,G2). gender(P,male) <=> male(P). gender(P,female) <=> female(P). male(P) <=> ~female(P). % seven rules :- kif_ain(((parent(M,C) & female(M)) <=> mother(M,C))). % ((parent(M,C) & female(M)) <=> mother(M,C)). :- is_entailed_u(((parent(M,C) & female(M)) <=> mother(M,C))). :- is_entailed_u(((parent(M,C) & female(M)) => mother(M,C))). % [ (not(female(M)):-not(mother(M, C)), parent(M, C)), % (not(parent(M, C)):-not(mother(M, C)), female(M)), % (mother(M, C):-parent(M, C), female(M)) % ]. :- is_entailed_u((mother(M,C) => (parent(M,C) & female(M)))). % [ (female(M):-mother(M, _C)), % (not(mother(M, _C)):-not(female(M))), % (not(mother(M, C)):-not(parent(M, C))), % (parent(M, C):-mother(M, C)) % ]. :- is_entailed_u(not(mother(M,C)):- not(parent(M,C))). :- is_entailed_u(not(mother(M,_Anyone)):- not(female(M))). :- is_entailed_u((parent(M,C):- mother(M,C))). :- is_entailed_u((female(M):- mother(M,_))). parent(GRAND,PARENT),parent(PARENT,CHILD) => grandparent(GRAND,CHILD). grandparent(X,Y),male(X) <=> grandfather(X,Y). grandparent(X,Y),female(X) <=> grandmother(X,Y). mother(Ma,Kid),parent(Kid,GrandKid) =>grandmother(Ma,GrandKid). grandparent(X,Y),female(X) <=> grandmother(X,Y). :- must(current_op(1150,_,(<=>))). (parent(X,Y),male(X) <=> father(X,Y)). (parent(Ma,X),parent(Ma,Y),different(X,Y) =>siblings(X,Y)). (parent(P1,P2) => ancestor(P1,P2)). (parent(P1,P2), ancestor(P2,P3)) => ancestor(P1,P3). (ancestor(P1,P2), ancestor(P2,P3)) => ancestor(P1,P3). mother(eileen,douglas). %= trudy is human human(trudy). %= catch a regression bug that may couse trudy to lose human assertion never_retract_u(human(trudy)). :- kif_ain(forall(p,exists([m,f], if(human(p), (mother(m,p) & father(f,p)))))). :- doall(dcall(father(_,trudy))). mother(trudy,eileen). ((human(P1),ancestor(P1,P2))=>human(P2)). % :- listing([ancestor,human,parent]). %=:- wdmsg("press Ctrl-D to resume."). %=:- prolog. grandmother(trudy,douglas). mother(trudy,robby). mother(trudy,liana). mother(liana,matt). mother(liana,liz). mother(trudy,pam). %= human(trudy) supports anscesteral rule that her decendants are humans as well .. therefore .. :- is_entailed_u(human(douglas)). /* ?- mpred_why(human(douglas)). Justifications for human(douglas): 1.1 ancestor(trudy,douglas) 1.2 human(trudy) 1.3 human(trudy),ancestor(trudy,douglas),{vg(s(douglas))}==>human(douglas) 2.1 ancestor(eileen,douglas) 2.2 human(eileen) 2.3 human(eileen),ancestor(eileen,douglas),{vg(s(douglas))}==>human(douglas) :- mpred_why(grandparent(trudy,douglas)). Justifications for grandparent(trudy,douglas): 1.1 grandmother(trudy,douglas) 1.2 grandmother(trudy,douglas),{vg(s(douglas,trudy))}==>grandparent(trudy,douglas) 2.1 parent(eileen,douglas) 2.2 parent(trudy,eileen) 2.3 parent(trudy,eilee.),parent(eileen,douglas),{vg(s(douglas,trudy))}==>grandparent(trudy,douglas) */ %=:- wdmsg("press Ctrl-D to resume."). :- style_check(-singleton). %= so far no males "asserted" in the KB :- doall(dcall(male(Who ))). /* OUTPUT WAS.. male(skArg1ofFatherFn(pam)). male(skArg1ofFatherFn(liz)). male(skArg1ofFatherFn(matt)). male(skArg1ofFatherFn(liana)). male(skArg1ofFatherFn(robby)). male(skArg1ofFatherFn(eileen)). male(skArg1ofFatherFn(douglas)). male(skArg1ofFatherFn(trudy)). */ %= we can report the presence on non male though... %= the ~/1 is our negation hook into the inference engine :- no_varnaming( mpred_no_chaining(doall((dcall(~male(Who )))))). %= we expect to see at least there mothers here %= succeed( ~male(liana)). %= succeed( ~male(trudy)). %= succeed( ~male(skArg1ofMotherFn(trudy))). %= succeed( ~male(eileen)). %= thus ~/1 is tnot/1 of XSB ?!? %= there ar explicly non females :- doall(dcall(~ female(Who ))). %= ensure skolems are made or destroyed father(robert,eileen). siblings(douglas,cassiopea). father(douglas,sophiaWebb). father(douglas,skylar). father(douglas,sophiaWisdom). father(douglas,zaltana).
:- is_entailed_u(human(douglas)).
:- mpred_why(human(douglas)). :- mpred_why(grandparent(trudy,douglas)). :- doall(dcall_test(mother(Female,Who))). :- doall(dcall_test(father(Male,Who))). % :- doall(dcall_test(male(Who))). % :- doall(dcall_test(female(Who))).
:- doall(dcall_test(siblings(Who,AndWho))).
%= human(P) => (female(P) v male(P)). :- kif_ain(if(gendered_human(P), (female(P) v male(P)))).