Microproject
Write a Clojure function which performs the not-elimination rule of inference described below in the main project. That is, write a Clojure function called not-elimination which takes a not expression as an argument, and returns a singleton set containing the result of not-elimination if the elimination rule applies, otherwise return the empty set.
Example usage:
|
1 2 3 4 5 6 7 8 |
(not-elimination '(not x)) => #{} (not-elimination '(not (not a))) => #{a} (not-elimination '(not (not (and a b)))) => #{(and a b)} (not-elimination '(not (not (not (not c))))) => #{(not (not c))} |
Main Project
In this project you will implement part of a propositional logic inference system in Clojure. Specifically, your system will perform not, and, and if-elimination using forward chaining inference. This means that given a proposition and a knowledge base of known facts, your system will derive all propositions which follow using the rules of inference.
You will implement four rules of inference:
- not-elimination: from (not (not X)), infer X
- and-elimination: from (and X Y), infer X and infer Y
- modus ponens: from (if X Y) and X, infer Y
- modus tollens: from (if X Y) and (not Y), infer (not X)
The main entry point for your program should be a function called fwd-infer which takes two arguments: a proposition, and a set of known facts (propositions). It should return the new knowledge base – that is, the originally known facts with the proposition and any newly inferred propositions added to it.
You might wish to start with the below skeleton for the program:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
(defn not-elimination [not-prop] ... ) (defn and-elimination [and-prop] ... ) (defn modus-ponens [if-prop kb] ... ) (defn modus-tollens [if-prop kb] ... ) (defn elim-step "One step of the elimination inference procedure." [prop kb] ... ) (defn fwd-infer [prop kb] ... ) |
Examples
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 |
(fwd-infer '(if a b) '#{(not b)}) Because: (if a b) and: (not b) I derived: (not a) by modus tollens => #{(if a b) (not a) (not b)} (fwd-infer 'a '#{(if a b) (if b c)}) Because: (if a b) and: a I derived: b by modus ponens Because: (if b c) and: b I derived: c by modus ponens => #{(if a b) a c (if b c) b} (fwd-infer-elim '(and (not (not (if a b))) a) '#{}) Because: (and (not (not (if a b))) a) I derived: (not (not (if a b))) and: a by and-elimination Because: (not (not (if a b))) I derived: (if a b) by not-elimination Because: (if a b) and: a I derived: b by modus ponens => #{(if a b) (not (not (if a b))) a (and (not (not (if a b))) a) b} |