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.
Resolution calculus, Tableaux, first order resolution
Hello,
after everything we have done with resolution calculus/tableaux/first order resolution I still have some problems to understand them like I should and I also have the feeling that I am not the only one with that problem.
Is it possible to upload for example 1 or 2 page pdf document (don’t ask for much), where you make an easy examples of them in a way that we can see clear the difference, how/when the rules are implemented and what is used when?
And best case would be, if you could give a brief explanation to every step why we do that step (or something like that).
OR maybe is better just to make an additional tutorial, where we go trough some examples?
Thanks in advance!
Challenge accepted. Give me an hour or so to TeX something
http://www.jazzpirate.com/Math/calculi_comparison.pdf
Let me know if there’s something that needs more explaining
2 „Gefällt mir“
Thanks! That explains a lot!
I would like to ask for only one more simpler Resolution example.
Something which is easier to follow and understand.
the thing about resolution is, it’s extremely schematic. Making the formula simpler doesn’t actually make the proof any simpler; all the steps are “the same”, there’s just potentially fewer of them.
Is there something specific you’d want elaborated? And where is the “problem”, in the CNF-algorithm that builds the clauses or the actual subsequent resolution? Or with the unification?
I will try again to understand it better and if there is a problem i will write again 
One question regarding the assignment 6:
in the exercise 6.3 → natural deduction: are we allowed to explain it with words (what we want/need to do) or we must use the syntax to explain it?
Thanks!
Syntax. Definitely. 
As “natural” as natural deduction wants to be, it is still a formal calculus made of well-defined rules acting on well-defined formal objects (i.e. formulae).
I have only one question regarding natural deduction:
How do we disprove with natural deduction?
I have not seen such example so it is somehow hard for me to imagine how we could do it… What we need to do in order to disprove something?
What do you mean by disprove? You can always prove not A for disprove A if you mean that.
Well… you don’t, depending on what you mean. A calculus fundamentally only ever has rules for proving a formula to be true, i.e. a tautology. It just so happens, that Tableaux and Resolution give you a failure condition - in the case of Tableaux, by constructing a counterexample, in the case of Resolution by having-exhausted-all-possible-resolutions.*
Natural Deduction does not.
eeeeh, careful here. The negation of „A is a tautology“ is not „NOT A is a tautology“. It might be the case that neither is true (if a formula is satisfiable, but not tautological).
- To be fair, in practice this isn’t actually as useful as one might think. If you do „proper mathematics“, you will have infinitely many axioms, so in theory infinitely many clauses to resolve / new assumptions to add in a Tableaux calculus. Provability in first-order logic in general is not computable.
Yeah but if you give us the task to prove or disprove a formula A, I hope it is either valid or not A is valid.
…no, definitely not 
To be fair though, if the assignment is „prove or disprove“, we don’t necessarily expect you to use a formal calculus, so you can do whatever. And looking for counterexamples first is usually a good strategy in that case. If we expect you to prove something in a formal calculus, the assignment is very likely „prove the following using calculus X…“