# Tag Info

Accepted

### Programming language prototyping in Mathematica

General Some general answers and comments first. 1 Are you aware of any projects using the Wolfram language resp. Mathematica as an environment to explore the design of programming languages - in ...
• 37.8k
Accepted

### The integer ababab (a,b>0) is always divisible by 7, without remainder

One may regard this question as the test of the system ability of proving theorems, but there is another view to understand what lies beneath this theorem. Then we figure out that the problem is quite ...
• 57.3k

### FindEquationalProof with Logic in Wolfram Mathematica

You don't need FindEquationalProof to this end, it is enough to use the quantifiers. ...
• 26.4k
Accepted

### Basic theorem proving in Mathematica?

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 ...
• 2,971

...
• 17.3k

### Proving uniqueness of group identity element

Let us consider the axioms for a group: groupTheory={ForAll[{a,b,c},g[a,g[b,c]]==g[g[a,b],c]], ForAll[a,g[a,e]==a], ForAll[a,g[a,inv[a]]==e]}; As shown in ...
• 10.2k

### Clues on theorem proving tools?

You can compose TautologyQ and Equivalent ClearAll[bEq] bEq = TautologyQ @* Equivalent; ...
• 396k
Accepted

### Verify triple product rule

The following is a automation of the proof here. No need to make use of $p V=R T$. eq = Dt@{z == z[x, y], y == y[x, z], x == x[y, z]} \begin{array}{l} dz=dx \frac{...
• 66.2k

### Solving a-two-variable equation in primes

FindInstance cannot prove that there are no solutions, especially when the domain of solutions is the set of primes. More acceptable approach would be: ...
• 57.3k

### FindEquationalProof to prove divisor theorem

This is more a draft answer to your question than a full answer. Two observations: first, while I'm hardly any expert on evaluation in Mathematica, Mathematica seems to try to evaluate the terms given ...
• 495

### Clues on theorem proving tools?

FindEquationalProof is available as an option: ...
• 495

### The integer ababab (a,b>0) is always divisible by 7, without remainder

Simplify[Mod[FromDigits[{a, b, a, b, a, b}], 7]==0, {a, b} âˆˆ PositiveIntegers] True BTW,...
• 73.1k
Accepted

### Solving a-two-variable equation in primes

Indeed, this can be done in one line: FindInstance[x^3 - y^4 == 1, {x, y}, Primes] {} No solution in the primes.
• 26.4k
Accepted

### Can we find validity proofs by means of rules of inference with FindEquationalProof?

Here you go. The definition of Boolean Logic comes directly from the documentation of FindEquationalProof: ...
• 495

### Verify triple product rule

Simplify[D[p[v, t], v]*D[v[p, t], t]*D[t[p, v], p],Assumptions -> p*v == r*t] (*-1*)

### Finding a root that makes this huge polynomial negative

Obviously you can not calculate differences with such high exponents using machine precision. Therefore you must rationalize your coefficients . However, your coefficients have only a limited ...
• 51.9k

### Derive Parseval's theorem in one dimension

The following is my trial for automating the manual deduction here. You can press Ctrl+Shift+t to transform the output to TraditionalForm to make it look good. <...
• 66.2k
Accepted

### Axiomatizing naturals

Here's a first draft of an answer. Induction will be used as the proof technique. Since Mathematica uses an equational prover, there's no direct way to use induction. What will be ventured here are ...
• 495

### How to deduce circle theorems in Wolfram language?

It seems that MMA can not find the general result but a special situation such as PlanarAngle equal to 30 Degree. Here is my test. ...
• 73.1k

### Why Can't Mathematica Resolve this Simple Quantified Expression?

There is a workaround. ClearAll[x, y]; ForAll[{x, y}, x > 0 && y > 0, x*Log[y] == y*Log[x]];Resolve[%, Reals] False
• 26.4k

### Implementing the field axioms with FindEquationalProof?

As I understand it, the field axioms cannot be axiomatized this way. But others are trying other ideas.
• 495

### Why Can't Mathematica Resolve this Simple Quantified Expression?

ContourPlot might help a little bit: ContourPlot[x^y == y^x, {x, 0, 2}, {y, 0, 2}, MaxRecursion -> 5,FrameLabel -> {x, y}] The only real solution(x>0,y>...

• 2,904

### How to deduce cosine theorem with vector?

Reduce can prove the cosine theorem but can not find the cosine theorem. ...
• 73.1k
1 vote
Accepted

### Proving conjecture on number series

First off I have not found a pattern yet (update: look at edit 2, I have found a general pattern), just a simplification by setting some parameters to 0. It's not really what you asked for since I am ...
• 3,748
1 vote

### Using the mathematical typography of formal logic

As mentioned by @CarlWoll in the comments, it comes down to the precedence of operators. ...
• 25.2k
1 vote
Accepted

### How to deduce cosine theorem with vector?

...
• 66.2k

Only top scored, non community-wiki answers of a minimum length are eligible