Merge pull request #5 from RAIRLab/Examples-and-Deadcode-trim

Examples and deadcode trim

problems/tutorial/DCEC.clj

@@ -0,0 +1,29 @@
+{:name "Belief follows from knowledge"
+ :description ""
+ :assumptions {1 (Knows! a P)}
+ :goal (Believes! a P)}
+
+ {:name "Conjunction under Belief"
+ :description ""
+ :assumptions {1 (Believes! a P)
+ 2 (Believes! a Q)}
+ :goal (Believes! a (and P Q))}
+
+ {:name "MP under Belief"
+ :description ""
+ :assumptions {1 (Believes! a1 t0 P)
+ 2 (Believes! a1 t0 (if P Q))}
+ :goal (Believes! a1 t0 Q)}
+
+{:name "Common Knowledge"
+ :description ""
+ :assumptions {1 (Common! t0 P)}
+ :goal (and (Knows! a1 t1 P) (Knows! a2 t1 P))}
+
+
+ {:name "Bird Theorem"
+ :description "Belief Conjunction and Truth from Knowledge"
+ :assumptions {1 (Believes! a P)
+ 2 (Believes! a Q)
+ 3 (if (Believes! a (and P Q)) (Knows! a R))}
+ :goal R}

problems/tutorial/PropositionalLogic.clj

@@ -0,0 +1,37 @@
+
+;;This file contains easy PC examples, including some PC infrence rules
+
+{:name "And Intro"
+ :description ""
+ :assumptions {1 P 2 Q}
+ :goal (and P Q)}
+
+{:name "And Elim Left"
+ :description ""
+ :assumptions {1 (and P Q)}
+ :goal P}
+
+{:name "And Elim Right"
+ :description ""
+ :assumptions {1 (and P Q)}
+ :goal Q}
+
+{:name "Or Intro Right"
+ :description ""
+ :assumptions {1 P}
+ :goal (or P Q)}
+
+{:name "Or Intro Left"
+ :description ""
+ :assumptions {1 P}
+ :goal (or Q P)}
+
+{:name "Or Elim"
+ :description ""
+ :assumptions {1 (or P Q) 2 (if P R) 3 (if Q R)}
+ :goal R}
+
+{:name "Green Cheese Moon"
+ :description "(if P (if Q P) is a tauto, its negation is a contradiction we can derive G from"
+ :assumptions {1 (not (if P (if Q P)))}
+ :goal G}