Is it possible to resolve this proposition?

up vote
2
down vote

favorite

Executing this code (see MSE for its background)

ForAll[a, b, c, Implies[ForAll[x, -1 <= x <= 1, RealAbs[a*x^2 + b*x + c] <= 1], 
 ForAll[x, -1 <= x <= 1, RealAbs[c*x^2 + b*x + a] <= 2]]]
Resolve[%, Reals]

, I obtain

Beep:The kernel Local has quit (exited) during the course of an evaluation.

Can somebody with a powerful comp kindly execute it and report us the result? It would be very kind of her/him.

asked Aug 26 at 6:20

user64494

2,6831917

3

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c] returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

1

Also: Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals] evaluates to True.
â€“Â kirma
Aug 26 at 10:31

@kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details?
â€“Â user64494
Aug 26 at 10:54

1

These are some of the things I'm worried about... but With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]] should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

1

x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right.
â€“Â kirma
Aug 26 at 18:14

Â |Â
show 3 more comments

up vote
2
down vote

favorite

Executing this code (see MSE for its background)

ForAll[a, b, c, Implies[ForAll[x, -1 <= x <= 1, RealAbs[a*x^2 + b*x + c] <= 1], 
 ForAll[x, -1 <= x <= 1, RealAbs[c*x^2 + b*x + a] <= 2]]]
Resolve[%, Reals]

, I obtain

Beep:The kernel Local has quit (exited) during the course of an evaluation.

Can somebody with a powerful comp kindly execute it and report us the result? It would be very kind of her/him.

asked Aug 26 at 6:20

user64494

2,6831917

3

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c] returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

1

Also: Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals] evaluates to True.
â€“Â kirma
Aug 26 at 10:31

@kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details?
â€“Â user64494
Aug 26 at 10:54

1

These are some of the things I'm worried about... but With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]] should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

1

x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right.
â€“Â kirma
Aug 26 at 18:14

Â |Â
show 3 more comments

up vote
2
down vote

favorite

Executing this code (see MSE for its background)

ForAll[a, b, c, Implies[ForAll[x, -1 <= x <= 1, RealAbs[a*x^2 + b*x + c] <= 1], 
 ForAll[x, -1 <= x <= 1, RealAbs[c*x^2 + b*x + a] <= 2]]]
Resolve[%, Reals]

, I obtain

Beep:The kernel Local has quit (exited) during the course of an evaluation.

Can somebody with a powerful comp kindly execute it and report us the result? It would be very kind of her/him.

asked Aug 26 at 6:20

user64494

2,6831917

Executing this code (see MSE for its background)

ForAll[a, b, c, Implies[ForAll[x, -1 <= x <= 1, RealAbs[a*x^2 + b*x + c] <= 1], 
 ForAll[x, -1 <= x <= 1, RealAbs[c*x^2 + b*x + a] <= 2]]]
Resolve[%, Reals]

, I obtain

Beep:The kernel Local has quit (exited) during the course of an evaluation.

Can somebody with a powerful comp kindly execute it and report us the result? It would be very kind of her/him.

asked Aug 26 at 6:20

user64494

2,6831917

asked Aug 26 at 6:20

user64494

2,6831917

asked Aug 26 at 6:20

user64494

2,6831917

asked Aug 26 at 6:20

user64494

2,6831917

3

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c] returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

1

Also: Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals] evaluates to True.
â€“Â kirma
Aug 26 at 10:31

@kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details?
â€“Â user64494
Aug 26 at 10:54

1

These are some of the things I'm worried about... but With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]] should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

1

x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right.
â€“Â kirma
Aug 26 at 18:14

Â |Â
show 3 more comments

3

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c] returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

1

Also: Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals] evaluates to True.
â€“Â kirma
Aug 26 at 10:31

@kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details?
â€“Â user64494
Aug 26 at 10:54

1

These are some of the things I'm worried about... but With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]] should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

1

x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right.
â€“Â kirma
Aug 26 at 18:14

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]

returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]

returns , which would imply that there are no results for which this implication wouldn't hold, or am I mistaken?
â€“Â kirma
Aug 26 at 10:24

Also:

Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals]

evaluates to True.
â€“Â kirma
Aug 26 at 10:31

Also:

Resolve[ForAll[a, b, c, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals]

evaluates to True.
â€“Â kirma
Aug 26 at 10:31

@kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details?
â€“Â user64494
Aug 26 at 10:54

These are some of the things I'm worried about... but

With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]]

should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

These are some of the things I'm worried about... but

With[eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, x, a, b, c]]

should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it?
â€“Â kirma
Aug 26 at 17:26

x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right.
â€“Â kirma
Aug 26 at 18:14

Â |Â
show 3 more comments

1 Answer
1

active

oldest

votes

up vote
5
down vote

accepted

Resolve[ForAll[a, b, c, 
 Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1],
 Reals], 
 Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], 
 Reals]]], Reals]

True

In addition to replacing RealAbs (which might complicate Resolve unnecessarily) with corresponding range checks, I Resolve parts of Implies early. These result somewhat complicated intermediate results, but apparently they're easier for top-level Resolve to handle than multiple ForAlls inside each other.

Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...

answered Aug 26 at 11:01

kirma

9,15112755

add a commentÂ |Â

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: "387"
;
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',
convertImagesToLinks: false,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
bindNavPrevention: true,
postfix: "",
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);

);

draft saved

draft discarded

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathematica.stackexchange.com%2fquestions%2f180667%2fis-it-possible-to-resolve-this-proposition%23new-answer', 'question_page');

);

Post as a guest

Name

1 Answer
1

active

oldest

votes

1 Answer
1

active

oldest

votes

up vote
5
down vote

accepted

Resolve[ForAll[a, b, c, 
 Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1],
 Reals], 
 Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], 
 Reals]]], Reals]

True

Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...

answered Aug 26 at 11:01

kirma

9,15112755

add a commentÂ |Â

up vote
5
down vote

accepted

Resolve[ForAll[a, b, c, 
 Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1],
 Reals], 
 Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], 
 Reals]]], Reals]

True

Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...

answered Aug 26 at 11:01

kirma

9,15112755

add a commentÂ |Â

up vote
5
down vote

accepted

Resolve[ForAll[a, b, c, 
 Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1],
 Reals], 
 Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], 
 Reals]]], Reals]

True

Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...

answered Aug 26 at 11:01

kirma

9,15112755

Resolve[ForAll[a, b, c, 
 Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1],
 Reals], 
 Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], 
 Reals]]], Reals]

True

Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...

answered Aug 26 at 11:01

kirma

9,15112755

answered Aug 26 at 11:01

kirma

9,15112755

answered Aug 26 at 11:01

kirma

9,15112755

answered Aug 26 at 11:01

kirma

9,15112755

add a commentÂ |Â

draft saved

draft discarded

draft saved

draft discarded

Post as a guest

Name

Search This Blog

Iyfjky