Some concrete questions about resolution method for predicate logic
$begingroup$
I think I understand the basics of it now, and when I practice on excersices and old exams it goes well most of the time. But I have some questions that I cant seem to find any straight forward answers to and it would help me so much if someone could help me out.
- In this picture enter image description here of an example I found he is using several "paths" and then he connects them. Is that something you can allways do? And am I right about that you can do it in several ways, so with only one path in this case?
- I asked this in another thread but I think it got too messy, because no one
really answered. But is it so that you dont have to use all the formulas in the resolution as long as you finish with an empty clause? For example if in the picture the solution had q(x) and -p(x) seperately, its enough to use one of them and in other words he could have taken p(a) against -p(x) and thats it?
logic predicate-logic
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
$endgroup$
add a comment |
$begingroup$
I think I understand the basics of it now, and when I practice on excersices and old exams it goes well most of the time. But I have some questions that I cant seem to find any straight forward answers to and it would help me so much if someone could help me out.
- In this picture enter image description here of an example I found he is using several "paths" and then he connects them. Is that something you can allways do? And am I right about that you can do it in several ways, so with only one path in this case?
- I asked this in another thread but I think it got too messy, because no one
really answered. But is it so that you dont have to use all the formulas in the resolution as long as you finish with an empty clause? For example if in the picture the solution had q(x) and -p(x) seperately, its enough to use one of them and in other words he could have taken p(a) against -p(x) and thats it?
logic predicate-logic
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
$endgroup$
add a comment |
$begingroup$
I think I understand the basics of it now, and when I practice on excersices and old exams it goes well most of the time. But I have some questions that I cant seem to find any straight forward answers to and it would help me so much if someone could help me out.
- In this picture enter image description here of an example I found he is using several "paths" and then he connects them. Is that something you can allways do? And am I right about that you can do it in several ways, so with only one path in this case?
- I asked this in another thread but I think it got too messy, because no one
really answered. But is it so that you dont have to use all the formulas in the resolution as long as you finish with an empty clause? For example if in the picture the solution had q(x) and -p(x) seperately, its enough to use one of them and in other words he could have taken p(a) against -p(x) and thats it?
logic predicate-logic
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
$endgroup$
I think I understand the basics of it now, and when I practice on excersices and old exams it goes well most of the time. But I have some questions that I cant seem to find any straight forward answers to and it would help me so much if someone could help me out.
- In this picture enter image description here of an example I found he is using several "paths" and then he connects them. Is that something you can allways do? And am I right about that you can do it in several ways, so with only one path in this case?
- I asked this in another thread but I think it got too messy, because no one
really answered. But is it so that you dont have to use all the formulas in the resolution as long as you finish with an empty clause? For example if in the picture the solution had q(x) and -p(x) seperately, its enough to use one of them and in other words he could have taken p(a) against -p(x) and thats it?
logic predicate-logic
logic predicate-logic
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
edited Dec 18 '18 at 15:53
Mauro ALLEGRANZA
66k449114
66k449114
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
asked Dec 18 '18 at 11:24
Jonatan HelenasonJonatan Helenason
12
12
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
See Resolution (logic) :
The resolution technique uses proof by contradiction.
The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.
In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $lnot p(x) lor q(x)$ and $lnot p(x) lor lnot q(x) lor r(x)$.
What we get is a new set of clauses :
1) $lnot p(a) lor lnot q(a) lor r(a)$
2) $p(a)$
3) $lnot r(a)$
4)$lnot p(a) lor q(a)$.
Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."
What we get is :
5) $lnot q(a) lor r(a)$ --- from 1) and 2)
6) $q(a)$ --- from 2) and 4)
7) $lnot q(a)$ --- from 3) and 5).
Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.
What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $lnot q(a)$.
But this amounts to $q(a) land lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.
Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.
Regarding :
you dont have to use all the formulas in the resolution as long as you finish with an empty clause?
the answer is : you dont.
The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."
But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
$endgroup$
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
|
show 2 more comments
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3045045%2fsome-concrete-questions-about-resolution-method-for-predicate-logic%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
See Resolution (logic) :
The resolution technique uses proof by contradiction.
The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.
In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $lnot p(x) lor q(x)$ and $lnot p(x) lor lnot q(x) lor r(x)$.
What we get is a new set of clauses :
1) $lnot p(a) lor lnot q(a) lor r(a)$
2) $p(a)$
3) $lnot r(a)$
4)$lnot p(a) lor q(a)$.
Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."
What we get is :
5) $lnot q(a) lor r(a)$ --- from 1) and 2)
6) $q(a)$ --- from 2) and 4)
7) $lnot q(a)$ --- from 3) and 5).
Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.
What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $lnot q(a)$.
But this amounts to $q(a) land lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.
Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.
Regarding :
you dont have to use all the formulas in the resolution as long as you finish with an empty clause?
the answer is : you dont.
The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."
But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
$endgroup$
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
|
show 2 more comments
$begingroup$
See Resolution (logic) :
The resolution technique uses proof by contradiction.
The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.
In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $lnot p(x) lor q(x)$ and $lnot p(x) lor lnot q(x) lor r(x)$.
What we get is a new set of clauses :
1) $lnot p(a) lor lnot q(a) lor r(a)$
2) $p(a)$
3) $lnot r(a)$
4)$lnot p(a) lor q(a)$.
Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."
What we get is :
5) $lnot q(a) lor r(a)$ --- from 1) and 2)
6) $q(a)$ --- from 2) and 4)
7) $lnot q(a)$ --- from 3) and 5).
Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.
What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $lnot q(a)$.
But this amounts to $q(a) land lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.
Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.
Regarding :
you dont have to use all the formulas in the resolution as long as you finish with an empty clause?
the answer is : you dont.
The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."
But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
$endgroup$
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
|
show 2 more comments
$begingroup$
See Resolution (logic) :
The resolution technique uses proof by contradiction.
The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.
In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $lnot p(x) lor q(x)$ and $lnot p(x) lor lnot q(x) lor r(x)$.
What we get is a new set of clauses :
1) $lnot p(a) lor lnot q(a) lor r(a)$
2) $p(a)$
3) $lnot r(a)$
4)$lnot p(a) lor q(a)$.
Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."
What we get is :
5) $lnot q(a) lor r(a)$ --- from 1) and 2)
6) $q(a)$ --- from 2) and 4)
7) $lnot q(a)$ --- from 3) and 5).
Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.
What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $lnot q(a)$.
But this amounts to $q(a) land lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.
Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.
Regarding :
you dont have to use all the formulas in the resolution as long as you finish with an empty clause?
the answer is : you dont.
The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."
But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
$endgroup$
See Resolution (logic) :
The resolution technique uses proof by contradiction.
The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set, it is added to it, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.
In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $lnot p(x) lor q(x)$ and $lnot p(x) lor lnot q(x) lor r(x)$.
What we get is a new set of clauses :
1) $lnot p(a) lor lnot q(a) lor r(a)$
2) $p(a)$
3) $lnot r(a)$
4)$lnot p(a) lor q(a)$.
Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."
What we get is :
5) $lnot q(a) lor r(a)$ --- from 1) and 2)
6) $q(a)$ --- from 2) and 4)
7) $lnot q(a)$ --- from 3) and 5).
Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.
What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $lnot q(a)$.
But this amounts to $q(a) land lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.
Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.
Regarding :
you dont have to use all the formulas in the resolution as long as you finish with an empty clause?
the answer is : you dont.
The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."
But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
answered Dec 18 '18 at 13:56
Mauro ALLEGRANZAMauro ALLEGRANZA
66k449114
66k449114
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
|
show 2 more comments
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Thank you very much. I think I get it. But instead of doing this unification in the beginning like that, it would also be possible to solve it using unifiers like (x:=a) when needed? And also if I understand you correctly, the unification we are talking about is also a step forward in process to produce the empty clause, so it is possible to "produce" clauses like that for use later in the process even without unification? If you understand what I meen?
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 19:13
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
Allso I have one last questions before my exam in 13 hours. In The example in this picture i.stack.imgur.com/zjg3k.png, what is it that makes 2 existental quantifiers both links to (a)? I know that when you have two allincluders connected with "and" you can put them as one, and two existental quantifiers can be put as one when connected with "or" . But why in this example? Would appritiate any input before my exam greatly!
$endgroup$
– Jonatan Helenason
Dec 18 '18 at 23:15
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
@JonatanHelenason - regarding the linked exerxise, the provided solution is wrong. You are right in saying that the the RH existential quantifiers are independent: thus, they must be instantiated with different values : $a$ and $b$.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:34
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
Then, it is enough $[x := a]$ in the LH formula to unify $q(a)$ with $lnot q(a)$ and get the empty clause.
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:35
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
$begingroup$
As said in my comment to your previous post : "The first formula is equivalent to $∀x[¬p(x) ∧ q(x)]$. From it alone it follows : $∀x q(x)$ and from it in turn $∀x q(x) ∨ ∀x s(x)$."
$endgroup$
– Mauro ALLEGRANZA
Dec 19 '18 at 9:37
|
show 2 more comments
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3045045%2fsome-concrete-questions-about-resolution-method-for-predicate-logic%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
