Mdthbs

Could flaps be raised upward to serve as spoilers / lift dumpers?

Does KNN have a loss function?

Windows del command not working?

How to structure presentation to avoid getting questions that will be answered later in the presentation?

Overprovisioning SSD on ubuntu. How? Ubuntu 19.04 Samsung SSD 860

Can you help me identify this set? (Emergency vehicles maybe?)

speaker impedence

How long should I wait to plug in my refrigerator after unplugging it?

Password management for kids - what's a good way to start?

Is this popular optical illusion made of a grey-scale image with coloured lines?

Why do we need a voltage divider when we get the same voltage at the output as the input?

How do I safety check that there is no light in Darkroom / Darkbag?

How does Rust's 128-bit integer `i128` work on a 64-bit system?

Is the EU really banning "toxic propellants" in 2020? How is that going to work?

Move label of an angle in Tikz

What is the difference between 2/4 and 4/4 when it comes the accented beats?

Can I say "Gesundheit" if someone is coughing?

Protect a 6 inch air hose from physical damage

Skipping same old introductions

Python π = 1 + (1/2) + (1/3) + (1/4) - (1/5) + (1/6) + (1/7) + (1/8) + (1/9) - (1/10) ...1748 Euler

What is realistic quality of computer blueprints quickly backed up before apocalypse and their impact on future design?

What is the reason behind water not falling from a bucket at the top of loop?

Selecting rows conflicting values in WHERE clause

Define tcolorbox in math mode

Basic theorem proving in Mathematica?

Proving uniqueness of group identity elementWhy Can't Mathematica Resolve this Simple Quantified Expression?Four color theorem in MathematicaImplicit Function Theorem

.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ margin-bottom:0;
}

3

1

$begingroup$

Let's say we have the following:

p is prime

n > 1   (n is an integer)

p = nq (I.e. p is a multiple of n)

It can be proved that p = n.

I've seen that Mathematica has some basic theorem proving capabilities (see the theorem-proving tag) via functions like Reduce.

Can Mathematica prove the above claim? Pointers to external resources are welcome.

theorem-proving

share|improve this question

edited 7 hours ago

dharmatech

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

$endgroup$

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  $begingroup$
  $p=5$, $q=3$, $n=5/3$, $p$ is not equal $n$. Maybe you forgot something?
  $endgroup$
  – yarchik
  8 hours ago
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @yarchik Yes you're right, thank you! n is an integer. I've updated the post.
  $endgroup$
  – dharmatech
  7 hours ago
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  $begingroup$
  Have a look at FindEquationalProof, though I think this may be harder than it looks.
  $endgroup$
  – Carl Lange
  7 hours ago
  

  
  
  
  

add a comment | 

3

1

$begingroup$

Let's say we have the following:

p is prime

n > 1   (n is an integer)

p = nq (I.e. p is a multiple of n)

It can be proved that p = n.

I've seen that Mathematica has some basic theorem proving capabilities (see the theorem-proving tag) via functions like Reduce.

Can Mathematica prove the above claim? Pointers to external resources are welcome.

theorem-proving

share|improve this question

edited 7 hours ago

dharmatech

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

$endgroup$

• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  $begingroup$
  $p=5$, $q=3$, $n=5/3$, $p$ is not equal $n$. Maybe you forgot something?
  $endgroup$
  – yarchik
  8 hours ago
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @yarchik Yes you're right, thank you! n is an integer. I've updated the post.
  $endgroup$
  – dharmatech
  7 hours ago
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  $begingroup$
  Have a look at FindEquationalProof, though I think this may be harder than it looks.
  $endgroup$
  – Carl Lange
  7 hours ago
  

  
  
  
  

add a comment | 

$begingroup$

Let's say we have the following:

p is prime

n > 1   (n is an integer)

p = nq (I.e. p is a multiple of n)

It can be proved that p = n.

I've seen that Mathematica has some basic theorem proving capabilities (see the theorem-proving tag) via functions like Reduce.

Can Mathematica prove the above claim? Pointers to external resources are welcome.

theorem-proving

share|improve this question

edited 7 hours ago

dharmatech

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

$endgroup$

p is prime

n > 1   (n is an integer)

p = nq (I.e. p is a multiple of n)

share|improve this question

edited 7 hours ago

dharmatech

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

share|improve this question

edited 7 hours ago

dharmatech

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

asked 9 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

1 Answer
1

active

oldest

votes

3

$begingroup$

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]



Failure["PropositionFalse", 

Association["MessageTemplate" -> TemplateObject[{

"The proposition could not be reduced to True."}

If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]

(*Same error as above*)



FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

As such one would have to build in the logic of multiplying for your theorem to be found.

share|improve this answer

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Excellent answer. Thank you!
  $endgroup$
  – dharmatech
  6 hours ago
  

  
  
  
  

add a comment | 

Your Answer

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


}
});

draft saved

draft discarded

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

Name

Email

Required, but never shown

StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathematica.stackexchange.com%2fquestions%2f203225%2fbasic-theorem-proving-in-mathematica%23new-answer', 'question_page');
}
);

Post as a guest

Name

Email

Required, but never shown

3

$begingroup$

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]



Failure["PropositionFalse", 

Association["MessageTemplate" -> TemplateObject[{

"The proposition could not be reduced to True."}

If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]

(*Same error as above*)



FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

As such one would have to build in the logic of multiplying for your theorem to be found.

share|improve this answer

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Excellent answer. Thank you!
  $endgroup$
  – dharmatech
  6 hours ago
  

  
  
  
  

add a comment | 

3

$begingroup$

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]



Failure["PropositionFalse", 

Association["MessageTemplate" -> TemplateObject[{

"The proposition could not be reduced to True."}

If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]

(*Same error as above*)



FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

As such one would have to build in the logic of multiplying for your theorem to be found.

share|improve this answer

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Excellent answer. Thank you!
  $endgroup$
  – dharmatech
  6 hours ago
  

  
  
  
  

add a comment | 

$begingroup$

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]



Failure["PropositionFalse", 

Association["MessageTemplate" -> TemplateObject[{

"The proposition could not be reduced to True."}

If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]

(*Same error as above*)



FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

As such one would have to build in the logic of multiplying for your theorem to be found.

share|improve this answer

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

$endgroup$

FindEquationalProof[a == b c, {a/c == b, c == 1}]



Failure["PropositionFalse", 

Association["MessageTemplate" -> TemplateObject[{

"The proposition could not be reduced to True."}

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]

(*Same error as above*)



FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

share|improve this answer

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges

answered 6 hours ago

morbomorbo

70233 silver badges99 bronze badges