Member since Apr 2018
15 posts

20190204, 21:15 #1
Subject: More Training Data for Exam Preparation [Logic]
+1 mecanum
I wanted to kindly ask whether it would be possible to provide us with more example logic problems, that are accompanied by solutions in the lecture's notation  specifically the kind which is similar to the following:
Problem 10.1 (Calculi Comparison) Problem 11.2 (FirstOrder Semantics) Problem 11.3 (Natural Deduction) Problem 12.2 (FirstOrder Resolution) Problem 12.3 (FirstOrder Tableaux) At least for me, access to more (and diverse examples) would greatly contribute to getting a finer intuition for the subtle differences between the used calculi. Edit: Also super appreciation is offered in exchange for the solution for Assignment 12 
This post was edited on 20190204, 21:48 by lu60ruhy.

Member since Oct 2014
93 posts

20190205, 06:26 #2
+5 LasagneAlForno, lu60ruhy, Marcel[Inf], Jazzpirate, Jonas S
>makes a post demanding for Data
>includes Star Trek Character which is not Data 0/10 meme potential used No, honestly, we will see if we have/find some more logic problems which are not used in your exam... 
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'."  Orteil, Creator of CookieClicker

Member since Oct 2016
803 posts

20190205, 11:06 #3
In reply to post #1
+1 lu60ruhy
You can easily generate infinitely many of them Any valid formula is a good example for resolution, natural deduction and tableau, any nonvalid formula is a good example for countermodel generation using tableau. Recall my previous post on algebraically handling formulas  you can easily use them to generated arbitrarily complex tautologies. https://fsi.cs.fau.de/forum/thread/16935Exercise101Tip… Another fun (and educational!) thing you can do is: Generate interesting formulas by running calculi backwards. For example, to generate an interesting tautology, start with an empty clause and "invent" clauses that resolve to the empty clause. Then invent clauses that resolve to the resulting clauses etc. Try to do nontrivial things  what do clauses have to look like such that they resolve to the empty (or previous) clauses and I need to unify terms? What if I have a skolem function here, what quantifiers does the resulting formula then have? Then try to prove that formula using a *different* calculus Use natural deduction without a specific goal to find a tautology, then prove it using tableau etc. All of this will not just give you infinitely many exercises for practicing calculi, but running things backwards will additionally give you a better intuition how any why that calculus works, what kinds of mistake you can make ("Wait, by running resolution backwards I seem to have generated a formula that isn't valid  where did I go wrong and why?") and as a result, you will be a lot faster in the exam 
Member since Oct 2016
803 posts

20190205, 11:10 #4
+1 lu60ruhy
Furthermore: Find a nontrivial formula "for each rule" in a calculus. If there's a side condition (e.g. "x may not occur freely in an open premise"), find situations where they don't apply and why applying the rule anyway would be a problem.
All of this is a lot more educational than If I were to just hand you formulas to mechanically prove  and counterintuitively, you will become better at proving things faster by going about it that way than by merely practicing proving things

This post was edited on 20190205, 11:29 by Jazzpirate.

Member since Apr 2018
15 posts

20190205, 11:48 #5
Thank you for your answer!
I'm afraid I have to disagree with you. If it were true, that your proposed way of generating the problems by one's self is the best way to gain an intuition into the calculi, you would probably have presented it this way in the exercises. I'm sure that it is a good way to deepen the understanding but at least I am not there yet. The fact that every additional source of similar problems outside the exercises uses a slightly different notation / terminology complicates grasping the essence of the calculi. As far as I can tell [RN] does not offer these kind of problems in the exercise part as well (maybe I am mistaken?). So before I can make the step to speeding up, I would very much like to verify my mental model of the calculi by training on examples that are accompanied by solutions with homogeneous notation that I can be confident in (contrary to solutions, which might be incorrect, because I 'invented' them myself  solving/running them in either direction). tl;dr: Let me get comfortable with the mechanical stuff first Thank you for your effort! 
This post was edited on 20190205, 11:53 by lu60ruhy.

Member since Oct 2016
803 posts

20190205, 12:03 #6
+1 lu60ruhy
Except that it's difficult to formualte and evaluate an exercise that basically amounts to "think for yourself" Exercises need to be selfcontained with an (ideally) clear instruction what you're expected to do and how the result will be graded. Fair point I'll see what I can do, but I have to admit that I'm pretty swamped at the moment, and nicely presenting formulas *and* their proofs in a given calculus takes a lot of time. I'll happily look over solutions that you or your coeds post in the forum, though. Perfectly correct  "Practice" goes beyond mere mechanics though. Sure, you can't fully understand a calculus without practicing it, but you can't understand a calculus by merely mechanically executing the algorithm over and over again either. Just as you can't become a good piano player without doing finger exercises, merely doing finger exercises won't make you a good piano player. 
Member since Apr 2018
15 posts

20190205, 13:58 #7
Maybe the tutors can help idk what they actually signed up for ... In the mean time at least the solution to Assignment 12 would be beneficial 
Member since Oct 2016
803 posts

20190205, 14:46 #8
+1 lu60ruhy

Member since Jul 2016
93 posts

20190205, 20:48 #9
You might find https://fsi.cs.fau.de/dw/pruefungen/bachelor#grundlagen_de… helpful.

Member since Apr 2018
15 posts

20190206, 15:28 #10
+1 Nash
Thanks for the advice! I had already looked into that, but unless I am missing something, the only accessible solutions there are a.) in a slightly different notation and b.) created by students (titled "solution attempts") which does not induce a lot of confidence (which is not a big deal, unless you are trying to learn this from scratch )
I know this sounds picky but I am convinced that these things matter when you are new to something. Consistency is king and errors in introductory material (or something that is used as such) pose considerable throwbacks when the student is trying to make sense of a concept. And I know that everybody (who puts in their time) will manage without the "extra training data" I asked for  but I am convinced, that it would help a lot of people get there faster. And thank you again for putting in thought and work (as much as it is possible  I know you have a lot to do elsewhere)! 
This post was edited on 20190206, 15:51 by lu60ruhy.

Member since Nov 2018
1 post

20190206, 17:22 #11
In reply to post #1
+1 lu60ruhy
I fully agree with you. I am also looking for some more exercises (especially for natural deduction in Gentzen notation) and reliable solutions. It is hard to figure out, how to proceed, if there are just a few examples. Every kind of exercise/ solution would be helpful for me. 
Member since Apr 2018
15 posts

20190206, 21:12 #12
Is the solution to Problem 5.2 (FirstOrder Tableau) (https://new.kwarc.info/teaching/AI/examWS201718withsol…) intentionally kept secret?

Member since Oct 2016
803 posts

20190207, 11:21 #13
I'll do it on a whiteboard and send you a photo, okay?

Member since Apr 2018
15 posts

20190207, 12:02 #14
A voice message would have been better, but if you insist ...

Member since Oct 2016
803 posts

20190207, 12:51 #15
+1 lu60ruhy

Datenschutz 
Kontakt
Powered by the Unclassified NewsBoard software, 20150713dev,
© 20032011 by Yves Goergen