Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
More Training Data for Exam Preparation [Logic]
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 (First-Order Semantics)
Problem 11.3 (Natural Deduction)
Problem 12.2 (First-Order Resolution)
Problem 12.3 (First-Order 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 
1 „Gefällt mir“
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…
5 „Gefällt mir“
You can easily generate infinitely many of them 
Any valid formula is a good example for resolution, natural deduction and tableau, any non-valid formula is a good example for counter-model generation using tableau.
Recall my previous post on algebraically handling formulas - you can easily use them to generated arbitrarily complex tautologies.
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 non-trivial 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
1 „Gefällt mir“
Furthermore: Find a non-trivial 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
1 „Gefällt mir“
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!
Except that it’s difficult to formualte and evaluate an exercise that basically amounts to „think for yourself“ Exercises need to be self-contained 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.
1 „Gefällt mir“
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
You might find https://fsi.cs.fau.de/dw/pruefungen/bachelor#grundlagen_der_logik_in_der_informatik_gloin helpful.
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)!
1 „Gefällt mir“
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.
1 „Gefällt mir“
Is the solution to Problem 5.2 (First-Order Tableau) (https://new.kwarc.info/teaching/AI/exam-WS2017-18-with-solutions.pdf) intentionally kept secret?
I’ll do it on a whiteboard and send you a photo, okay? 
A voice message would have been better, but if you insist …
1 „Gefällt mir“
For natural deduction I found these examples very helpful:
2 „Gefällt mir“
That looks awesome
One more comment on my hand-scribbled solution for 5.2:
Note that since I instantiated X with b in the left branch of the tableau-proof, I have to instantiate X in the right branch by the same value b (it’s not really made clear in my proof, sorry about that). That’s because a substitution applies to all formulas resulting from an elimination of a quantifier, which in this case is right in the first step of the proof, whereas the quantifier binding Y is eliminated separately in each branch (hence I may substitute Y by different values in both branches).
If I wanted to instantiate X by a different value in the right branch, I would have to reliminate the \exists X again in the right branch, forcing me to redo all of the steps above the branching step, which wouldn’t help me in this particular proof.
Have you seen the examples here (PL):
https://leanprover.github.io/logic_and_proof/natural_deduction_for_propositional_logic.html
and here (FOL):
https://leanprover.github.io/logic_and_proof/natural_deduction_for_first_order_logic.html
?
The calculus is slightly different (No TND but a few more rules) but the notation is very similar.