proof by finding suitable instances and resolution
$begingroup$
I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 << x_2 * y_2}; {x_2 not<< y_2, x_2 + y_2 <<< x_2 * y_2}; {x not<<< y}}$
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.
I don't manage to find suitable instances of the clauses. Do you have any idea?
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?
I'd appreciate your help on this! :)
logic propositional-calculus first-order-logic predicate-logic proof-theory
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
$endgroup$
add a comment |
$begingroup$
I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 << x_2 * y_2}; {x_2 not<< y_2, x_2 + y_2 <<< x_2 * y_2}; {x not<<< y}}$
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.
I don't manage to find suitable instances of the clauses. Do you have any idea?
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?
I'd appreciate your help on this! :)
logic propositional-calculus first-order-logic predicate-logic proof-theory
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
$endgroup$
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06
add a comment |
$begingroup$
I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 << x_2 * y_2}; {x_2 not<< y_2, x_2 + y_2 <<< x_2 * y_2}; {x not<<< y}}$
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.
I don't manage to find suitable instances of the clauses. Do you have any idea?
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?
I'd appreciate your help on this! :)
logic propositional-calculus first-order-logic predicate-logic proof-theory
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
$endgroup$
I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 << x_2 * y_2}; {x_2 not<< y_2, x_2 + y_2 <<< x_2 * y_2}; {x not<<< y}}$
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.
I don't manage to find suitable instances of the clauses. Do you have any idea?
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?
I'd appreciate your help on this! :)
logic propositional-calculus first-order-logic predicate-logic proof-theory
logic propositional-calculus first-order-logic predicate-logic proof-theory
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
edited Dec 9 '18 at 22:37
Studentu
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
asked Dec 9 '18 at 20:37
StudentuStudentu
1229
1229
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06
add a comment |
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 ll x_2 * y_2}; {x_2 notll y_2, x_2 + y_2 lll x_2 * y_2}; {x notlll y}}$
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
begin{align*}
& a+b < a*b\\
& a+b not< a*b\
& (a+b) + (a*b) ll (a+b) * (a*b)\\
& (a+b) + (a*b) notll (a+b) * (a*b)\
& ((a+b)+(a*b))+((a+b)*(a*b)) lll ((a+b)+(a*b))*((a+b)*(a*b))\\
& ((a+b)+(a*b))+((a+b)*(a*b)) notlll ((a+b)+(a*b))*((a+b)*(a*b))\\
end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
begin{align*}
&{a+b <_1 a*b}\
%
&{x_k not<_{(k-1)} y_k, x_k + y_k <_k x_k * y_k}quad 1<k<n\
&{x_{n} not<_{n-1}< y_{n}}
end{align*}
and to instantiate the free variables consider terms,
$s_0 = a$,
$t_0 = b$,
$s_k =s_{(k-1)}+t_{(k-1)}$ and
$t_k =s_{(k-1)}*t_{(k-1)}$,
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
$endgroup$
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
|
show 5 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%2f3032966%2fproof-by-finding-suitable-instances-and-resolution%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$
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 ll x_2 * y_2}; {x_2 notll y_2, x_2 + y_2 lll x_2 * y_2}; {x notlll y}}$
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
begin{align*}
& a+b < a*b\\
& a+b not< a*b\
& (a+b) + (a*b) ll (a+b) * (a*b)\\
& (a+b) + (a*b) notll (a+b) * (a*b)\
& ((a+b)+(a*b))+((a+b)*(a*b)) lll ((a+b)+(a*b))*((a+b)*(a*b))\\
& ((a+b)+(a*b))+((a+b)*(a*b)) notlll ((a+b)+(a*b))*((a+b)*(a*b))\\
end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
begin{align*}
&{a+b <_1 a*b}\
%
&{x_k not<_{(k-1)} y_k, x_k + y_k <_k x_k * y_k}quad 1<k<n\
&{x_{n} not<_{n-1}< y_{n}}
end{align*}
and to instantiate the free variables consider terms,
$s_0 = a$,
$t_0 = b$,
$s_k =s_{(k-1)}+t_{(k-1)}$ and
$t_k =s_{(k-1)}*t_{(k-1)}$,
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
$endgroup$
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
|
show 5 more comments
$begingroup$
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 ll x_2 * y_2}; {x_2 notll y_2, x_2 + y_2 lll x_2 * y_2}; {x notlll y}}$
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
begin{align*}
& a+b < a*b\\
& a+b not< a*b\
& (a+b) + (a*b) ll (a+b) * (a*b)\\
& (a+b) + (a*b) notll (a+b) * (a*b)\
& ((a+b)+(a*b))+((a+b)*(a*b)) lll ((a+b)+(a*b))*((a+b)*(a*b))\\
& ((a+b)+(a*b))+((a+b)*(a*b)) notlll ((a+b)+(a*b))*((a+b)*(a*b))\\
end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
begin{align*}
&{a+b <_1 a*b}\
%
&{x_k not<_{(k-1)} y_k, x_k + y_k <_k x_k * y_k}quad 1<k<n\
&{x_{n} not<_{n-1}< y_{n}}
end{align*}
and to instantiate the free variables consider terms,
$s_0 = a$,
$t_0 = b$,
$s_k =s_{(k-1)}+t_{(k-1)}$ and
$t_k =s_{(k-1)}*t_{(k-1)}$,
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
$endgroup$
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
|
show 5 more comments
$begingroup$
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 ll x_2 * y_2}; {x_2 notll y_2, x_2 + y_2 lll x_2 * y_2}; {x notlll y}}$
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
begin{align*}
& a+b < a*b\\
& a+b not< a*b\
& (a+b) + (a*b) ll (a+b) * (a*b)\\
& (a+b) + (a*b) notll (a+b) * (a*b)\
& ((a+b)+(a*b))+((a+b)*(a*b)) lll ((a+b)+(a*b))*((a+b)*(a*b))\\
& ((a+b)+(a*b))+((a+b)*(a*b)) notlll ((a+b)+(a*b))*((a+b)*(a*b))\\
end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
begin{align*}
&{a+b <_1 a*b}\
%
&{x_k not<_{(k-1)} y_k, x_k + y_k <_k x_k * y_k}quad 1<k<n\
&{x_{n} not<_{n-1}< y_{n}}
end{align*}
and to instantiate the free variables consider terms,
$s_0 = a$,
$t_0 = b$,
$s_k =s_{(k-1)}+t_{(k-1)}$ and
$t_k =s_{(k-1)}*t_{(k-1)}$,
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
$endgroup$
proof by resolution that the following CNF is unsatisfiable:
${{a+b < a*b}; {x_2 not< y_2, x_2 + y_2 ll x_2 * y_2}; {x_2 notll y_2, x_2 + y_2 lll x_2 * y_2}; {x notlll y}}$
You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,
begin{align*}
& a+b < a*b\\
& a+b not< a*b\
& (a+b) + (a*b) ll (a+b) * (a*b)\\
& (a+b) + (a*b) notll (a+b) * (a*b)\
& ((a+b)+(a*b))+((a+b)*(a*b)) lll ((a+b)+(a*b))*((a+b)*(a*b))\\
& ((a+b)+(a*b))+((a+b)*(a*b)) notlll ((a+b)+(a*b))*((a+b)*(a*b))\\
end{align*}
Applying the resolution method is now trivial.
For question number 2 consider,
begin{align*}
&{a+b <_1 a*b}\
%
&{x_k not<_{(k-1)} y_k, x_k + y_k <_k x_k * y_k}quad 1<k<n\
&{x_{n} not<_{n-1}< y_{n}}
end{align*}
and to instantiate the free variables consider terms,
$s_0 = a$,
$t_0 = b$,
$s_k =s_{(k-1)}+t_{(k-1)}$ and
$t_k =s_{(k-1)}*t_{(k-1)}$,
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
edited Dec 10 '18 at 10:55
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
answered Dec 9 '18 at 23:31
Jorge AdrianoJorge Adriano
59146
59146
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
|
show 5 more comments
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
1
1
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
$begingroup$
Indeed that's what I did. A set such as ${x2≪̸y2,x2+y2⋘x2∗y2}$ is typically a a schema, that is shorthand notation for a union $bigcup{{x2≪̸y2,x2+y2⋘x2∗y2} | x2, y2 in mathcal{D}}$ where $mathcal{D}$ is their domain.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:09
1
1
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
$begingroup$
That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:17
1
1
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
$begingroup$
For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles.
$endgroup$
– Jorge Adriano
Dec 10 '18 at 1:31
1
1
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
$begingroup$
edited with some detail on question 2
$endgroup$
– Jorge Adriano
Dec 10 '18 at 2:31
1
1
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
$begingroup$
Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial).
$endgroup$
– Jorge Adriano
Dec 10 '18 at 10:57
|
show 5 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%2f3032966%2fproof-by-finding-suitable-instances-and-resolution%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
$begingroup$
If anything is unclear in my post, please let me know.
$endgroup$
– Studentu
Dec 9 '18 at 22:06