Johnbeve main (#4)

* Typo fix (#5) The project was copy-and-pasted, but not all deets were updated to reflect the project is the 2nd one * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Update README.md * Create README.md * Update README.md Fixed question 8 based on Jieming's note. * Update README.md You can tag your peers in a commit @jonathanvajda @SydCo99 @giacomodecolle @oliviahobai @Jiemingy @JaronJCheung If you want someone to look over your work before you open a pull request, just tag them in the commit. * Add proj1 * Delete Peihong_Xie_Project_1_50375781.md Hi there, Merging to my repository is what we'll be doing next week. This week, I'd like you to open a pull request in your _own_ repository, then assign it to at least two of your peers from class. You'll all then review your updates, and once your reviewers give you the green light, you'll merge your changes to your branch, then open a pull request for me to review. -John * Delete fitch_proof_1.PNG * Delete fitch_proof_2.PNG * Delete fitch_proof_3.PNG * Delete fitch_proof_4.PNG * Delete tree_proof_1.png * Delete tree_proof_2.png * Delete tree_proof_3.png * Delete tree_proof_4.png * Create README.md * Update README.md * Update README.md * Update README.md --------- Co-authored-by: Jonathan Vajda <[email protected]> Co-authored-by: Jiemingy <[email protected]> Co-authored-by: John Beverley <[email protected]>
johnbeve · Feb 14, 2023 · 4d8ff17 · 4d8ff17
1 parent 13aae61
commit 4d8ff17
Show file tree

Hide file tree

Showing 3 changed files with 90 additions and 10 deletions.
diff --git a/Project-1/README.md b/Project-1/README.md
@@ -0,0 +1,76 @@
+# Project 1 Assignment
+
+Your first project will require you to answer each of the 10 questions below.  You will be expected to open a pull request with your initial answers by the second class meeting, giving you one week to work on these problems. You and your peers will then have one week to work together to refine your respective initial answers, so they are ready for final submission. Once your pull requests have been reviewed and merged to the development branch, I will review them, then merge to the master branch. 
+
+```
+Tip #1: Carefully study the Hedman selections assigned, as several of the questions are taken directly from the textbook. 
+Tip #2: Google is your friend. An important skill to pick up in this class is recognizing when to think hard and when to think smart. You might find answers to some of the questions below simply by googling; you might find pieces of answers to parts of some question below, which will need to be combined; then again, you might not find any help at all because the questions are more novel than they initially appear. I encourage you to use existing resources as guidance, but be careful. My reputation for asking students tricky questions is well-earned. 
+Tip #3: Work _together_ to solve these problems, even for initial submissions and when you do, document this in github. For example, you might feel like you nearly have answers to question 1, but would love another pair of eyes. You can then open a post in your local github account, and tag folks from class requesting they check out your work. 
+Tip #4: The work we do is challenging; that should be assumed. You are smart enough to be here; that should also be assumed. We have neither time nor space for shaming, but all of time and space for praising. Be cognizant of how your messages might be received, and err on the side of caution. It is hard to surmise intent from text alone. For my part, I treat text only communications the way modern musicals are written: Little subtext; emotions on the sleeve. 
+```
+
+Note: The standard interpretation of the logical symbols - "∨", "∧", "→", "¬", "∀", "∃" - is assumed throughout. 
+
+1. Provide the truth tables for each of the following propositional logic formulas. State whether each is a tautology, a contradiction, or contingent:
+  ```
+  (a) (¬A→B)∨((A∧¬C)→B) 
+  (b) (A→B)∧(A→¬B)
+  (c) (A→(B∨C))∨(C→¬A) 
+  (d) ((A→B)∧C)∨(A∧D) 
+  ```
+
+2. A _literal_ is an atomic formula or the negation of an atomic formula. We say a formula is in _conjunctive normal form_ (CNF) if it is the conjunction of the disjunction of literals. Find propositional logic formulas in CNF equivalent to each of the following:
+  ```
+  (a) (A→B)→C
+  (b) (A→(B∨C))∨(C→¬A)
+  (c) (¬A∧¬B∧C)∨(¬A∧¬C)∨(B∧C)∨A 
+  ```
+
+3. Let V be the vocabulary of first-order logic consisting of a binary relation P and a unary relation F. Interpret P(x,y) as “x is a parent of y” and F(x) as “x is female.” Where possible define the following formulas in this vocabulary; where not possible, explain why: 
+
+  ```
+  (a)  B(x,y) that says that x is a brother of y  
+  (b)  A(x,y) that says that x is an aunt of y  
+  (c)  C(x,y) that says that x and y are cousins   
+  (d)  O(x) that says that x is an only child  
+  (e)  T(x) that says that x has exactly two brothers 
+  ```
+
+4. Let V be a vocabulary of the attribute (concept) language with complements (ALC) consisting of a role name "parent_of" and a concept name "Male". Interpret parent_of as "x is a parent of y" and M as "x is male". Where possible define the following formulas in this vocabulary; where not possible, explain why: 
+  ```
+  (a)  B that says that x is a brother of y
+  (b)  A that says that x is an aunt of y
+  (c)  C that says that x and y are cousins
+  (d)  O that says that x is an only child  
+  (e)  T that says that x has exactly two brothers 
+  ```
+
+
+5. Select two formulas defined in ALC from question 4 to form the basis of a T-Box. Supplement this T-box with whatever other axioms you like, as well as an A-box, so that you ultimately construct a knowledge base K = (T,A). Provide a _model_ of K. This may be graphical or symbolic or both. 
+
+6. Explain the difference - using natural language - between the first-order prefixes:
+  ```
+  (a) ∃x∀y and ∀x∃y
+  (b) ∃x∀y∃z and ∀x∃y∀z 
+  (c) ∀x∃y∀z∃w and ∃x∀y∃z∀w
+```
+
+7. Show that the following sentences are not equivalent by exhibiting a graph that models one but not both of these sentences:
+```
+∀x∃y∀z(R(x,y) ∧ R(x,z) ∧ R(y,z))
+∃x∀y∃z(R(x,y) ∧ R(x,z) ∧ R(y,z))
+```
+
+8. Using an online tableau proof generator - such as the one found here `https://www.umsu.de/trees/` - provide tree proofs of the following entailments, which are known as the De Morgan's laws:
+  ```
+  (a) ∀x∀y(¬(Px ∧ Qx) → (¬Px ∨ ¬Qx))
+  (b) ∀x∀y(¬(Px ∨ Qx) → (¬Px ∧ ¬Qx))
+  (c) ∀x∀y((¬Px ∨ ¬Qx) → ¬(Px ∧ Qx))
+  (d) ∀x∀y((¬Px ∧ ¬Qx) → ¬(Px ∨ Qx))
+```
+
+9. Using a natural deduction proof generator - such as the one found here `https://proofs.openlogicproject.org/` - provide natural deduction proofs for each of De Morgan's laws. 
+
+10. Compare and contrast the proofs provided for (a) in your answers to questions 8 and 9. Explain the different assumptions, strategies, etc. exhibited in tree proofs vs natural deduction proofs. 
+
+
diff --git a/Project-2/README.md b/Project-2/README.md
@@ -5,8 +5,8 @@ Your second project will require you to answer each of the 10 questions below.
 ```
 Tip #1: Carefully study the Baader, et. al. selections assigned on bisimulation; it is deceptively subtle, and quite powerful. 
 Tip #2: Google is still your friend. So is stackexchange...
-Tip #3: Work _together_ to solve these problems, even for initial submissions and when you do, document this in github. 
-Tip #4: Work together _as a team_. 
+Tip #3: Work together to solve these problems, even for initial submissions and when you do, document this in github. 
+Tip #4: Work together as a team. 
 ```
 
 1. Let V be a vocabulary of ALCI consisting of a role name "P". Interpret part_of as "x is a part of y". Using this role name, define the following formulas in this language:
@@ -20,30 +20,31 @@ Tip #4: Work together _as a team_.
 
 2. Use your axioms from question 1 as the basis of an ALCI T-Box. Supplement this T-box with whatever other axioms you like, as well as an A-box, so that you ultimately construct a knowledge base K = (T,A). Provide a _model_ of K. This may be graphical or symbolic or both. 
 
-3. Translate the following first-order logic axioms into ALC: 
+3. Translate the following first-order logic axioms into ALCI: 
 ```
 (a) ∀x∃y∀z(R(x,y) ∧ R(x,z) ∧ R(y,z))
 (b) ∃x∀y∃z(R(x,y) ∧ R(x,z) ∧ R(y,z))
 (c) ∀y(R(x, y) → ∃x(R(y, x) ∧ ∀y(R(x, y) → A(y))))
 (d) (∀y)(R(x, y) → A(y)) ∧ (∃y)(R(x, y) ∧ B(y))
 ```
-4. Provide an interpretation I<sub>1</sub> for ALC and an interpretation I<sub>2</sub> for ALCN - each distinct from any interpretation covered in class so far - and construct a bisimulation that demonstrates ALCN is more expressive than ALC. Use the [mermaid syntax](https://github.com/mermaid-js/mermaid) of markdown to provide a graphical representation of your work. 
+4. Provide an interpretation I<sub>1</sub> for ALC and an interpretation I<sub>2</sub> for ALCN - each distinct from any interpretation covered in class so far - and construct a bisimulation that demonstrates ALCN is more expressive than ALC. Use the [mermaid syntax](https://github.com/mermaid-js/mermaid) of markdown to provide a graphical representation of your work. Feel free to use the [mermaid live editor](https://mermaid.live/) when diagramming. 
 
-5. Provide an interpretation I<sub>1</sub> for ALC and an interpretation I<sub>2</sub> for ALCN - each distinct from any interpretation covered in class so far - and construct a bisimulation that _does not_ demonstrate ALCN is more expressive than ALC. Use the [mermaid syntax](https://github.com/mermaid-js/mermaid) of markdown to provide a graphical representation of your work. 
+5. Provide an interpretation I<sub>1</sub> for ALC and an interpretation I<sub>2</sub> for ALCN - each distinct from any interpretation covered in class so far - and construct a bisimulation that _does not_ demonstrate ALCN is more expressive than ALC. Use the [mermaid syntax](https://github.com/mermaid-js/mermaid) of markdown to provide a graphical representation of your work. Feel free to use the [mermaid live editor](https://mermaid.live/) when diagramming. 
 
 
-6. Explain the difference - using natural language - between the first-order prefixes:
+6. Explain the difference - using natural language - between the description logic expressions:
   ```
-  (a) ∃x∀y and ∀x∃y
-  (b) ∃x∀y∃z and ∀x∃y∀z 
-  (c) ∀x∃y∀z∃w and ∃x∀y∃z∀w
+  (a) ∃r.C and ∀r.C
+  (b) ∃r-.C and ∀r-.C
+  (c) <=nr and <=nr.C
+  (d) ∃r-.C and ∃r-.{a} 
 ```
 
 7. There is a delightfully helpful subreddit called "ELI5" which stands for something like "explain it like I'm 5" where users post conceptually challenging questions and other users attempt to provide explanations in simple, jargon-free, terms that presumably a 5 year-old could understand. Using this as a model, explain the _finite model property_. Be sure to provide a simple example and explain when the property might be important, and when it is not so important. 
 
 8. Following up on the preceding , explain the _tree model property_. Be sure to provide a simple example and explain when the property might be important, and when it is not so important. 
 
-9. Open the Protege editor and create object properties for each of the role names that you constructed in question 1. You should have at least 6 object properties. Assert in the editor that P is a sub-property of O, that P is transitive, and that O is symmetric. Next, add individuals - a, b, c - to the file and assert that c is part of a and that c overlaps b. Running the reasoner should reveal - highlighted in yellow if you select the individual c - that c overlaps a. Using the discussion in the selections from chapter 4 of the Baader, et. al. text as a guide, explain how the tableau algorithm is generating this inference. 
+9. Open the Protege editor and create object properties for each of the role names that you constructed in question 1. You should have at least 6 object properties. Assert in the editor that P is a sub-property of O, that P is transitive, and that O is symmetric. Next, add individuals - a, b, c - to the file and assert that c is part of a and that c overlaps b. Running the reasoner should reveal - highlighted in yellow if you select the individual c - that c overlaps a. Using the discussion in the selections from chapter 4 of the Baader, et. al. text as a guide, explain how the tableau algorithm is generating this inference. Also, provide a screenshot of the results of your reasoner run with c highlighted. 
 
 10. Following up on your work in question 9, adjust/add/remove/etc. object properties and individuals in your Protege file so that when you run a reasoner in Protege, you return the following consequences: 
 ```
@@ -52,3 +53,4 @@ Tip #4: Work together _as a team_.
   (c) a is part of b, b is part of f, and a is part of f
   (e) There are no parts between a and g in common
 ```
+Provide a screenshot of your results here. 
diff --git a/Project-3/README.md b/Project-3/README.md
@@ -0,0 +1,2 @@
+
+You know what's coming...