Mfcttrf

Declaring a visitor to the UK as my "girlfriend" - effect on getting a Visitor visa?

How can a class have multiple methods without breaking the single responsibility principle

Is verification of a blockchain computationally cheaper than recreating it?

How do I solve such questions on paramagnetism and ferromagnetism?

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

Does the use of a new concept require a prior definition?

How did Biff return to 2015 from 1955 without a lightning strike?

How to get maximum number that newcount can hold?

Can Otiluke's Freezing Spheres be stockpiled?

Reasons for using monsters as bioweapons

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

Is the un-detonated globe of Otiluke's Freezing Sphere magical?

"Will flex for food". What does this phrase mean?

Went to a big 4 but got fired for underperformance in a year recently - Now every one thinks I'm pro - How to balance expectations?

A conjectural trigonometric identity

How is Sword Coast North governed?

Applying for mortgage when living together but only one will be on the mortgage

HackerRank Implement Queue using two stacks Solution

How to avoid a lengthy conversation with someone from the neighborhood I don't share interests with

Has J.J.Jameson ever found out that Peter Parker is Spider-Man?

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

cannot trash malware NGPlayerSetup.dmg

Skipping same old introductions

The grades of the students in a class

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 8 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
  7 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
  6 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 8 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
  7 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
  6 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 8 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 8 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

share|improve this question

edited 7 hours ago

dharmatech

asked 8 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

asked 8 hours ago

dharmatechdharmatech

45611 gold badge99 silver badges1818 bronze badges

asked 8 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