# LogicMOO Programming Defeasible logic is a non-monotonic logic proposed by Donald Nute to formalize defeasible reasoning. In defeasible logic, there are three different types of propositions: * strict rules - specify that a fact is always a consequence of another; * defeasible rules - specify that a fact is typically a consequence of another; * undercutting defeaters - specify exceptions to defeasible rules. A priority ordering over the defeasible rules and the defeaters can be given. During the process of deduction, the strict rules are always applied, while a defeasible rule can be applied only if no defeater of a higher priority specifies that it should not. 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_repl) provides Toplevel Interaction. - library(logicmoo_plarkc) provides DEL Logic. - 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.

More examples found in these files: