Questions tagged [theorem-proving]
The theorem-proving tag has no usage guidance.
33
questions
0
votes
0
answers
38
views
Symbolic solutions to systems of Boolean constraints?
Is it possible to solve a system of Boolean constraints symbolically? I'm trying to solve systems like the following, where $X$ is the unknown Boolean expression I'm trying to find, $a, b, c$ are the ...
- 440
1
vote
2
answers
93
views
Solving a-two-variable equation in primes
How solve the following equation in Mathematica (preferably in one line) for pairs of $(x,y)$ such that $x$ and $y$ are primes?
$x^3-y^4=1$
- 115
1
vote
1
answer
99
views
Is there any Mathematica API for Z3?
Z3 has bindings for various programming languages, e.g., C, C++, Java, Python, and so on. Are there any for Mathematica? Or how to implement one?
- 840
-3
votes
1
answer
290
views
Proving conjecture on number series
I have a conjecture that Stephen Lucas's identities for Pi and its convergent could be generalized as follows:
...
- 51
0
votes
0
answers
25
views
How can I combine an identity predicate with first-order predicates while using FindEquationalProof
I am trying out some of the automated theorem proving in mathematica, and for my test case am working with Tarski and Sczerba's (mostly) first-order axiomatization of Affine Geometry, which has just ...
2
votes
1
answer
116
views
Derive Parseval's theorem in one dimension
Parseval's theorem (in one dimension) is a fundamental result in the theory of Fourier transforms. If $f(t) \Leftrightarrow F(\omega )$ are Fourier transform pairs and $t$ (time) and $\omega$ (...
- 39.9k
1
vote
0
answers
122
views
0
votes
1
answer
80
views
Using the mathematical typography of formal logic
As asked in this question, I strongly prefer to use "mathematical" typography in Mathematica over text-based ("computer science") typography. Nevertheless, it sometimes fails for ...
- 39.9k
0
votes
0
answers
62
views
Can Mathematica’s automated theorem prover and assistant work with the axioms of real (or complex) numbers?
axioms of real numbers
The question pretty much says it all. If I can make Mathematica do simple limit proofs that would be a good start.
Of course what I’d really like to do is turn this loose on the ...
- 85
3
votes
0
answers
70
views
Can I use FindInstance to prove an algebraic identity?
This question arose from a [now removed] MathOverflow discussion, where a Null result from a FindInstance query was used to prove that $f(x_1,x_2,\ldots x_n)\neq 0$ has no solution in $\mathbb{R}$. My ...
- 913
1
vote
2
answers
178
views
6
votes
3
answers
1k
views
The integer ababab (a,b>0) is always divisible by 7, without remainder
The integer $ababab$ $(a>0,b>0)$ is always divisible by $7$, without rest.
I tried to prove this by:
...
- 11.6k
3
votes
3
answers
325
views
Verify triple product rule
I'm trying to verify triple product rule
$$\left(\frac{\partial x}{\partial y}\right) \left(\frac{\partial y}{\partial z}\right) \left(\frac{\partial z}{\partial x}\right) = -1$$
with the equation:
<...
- 1,943
2
votes
2
answers
96
views
How to deduce cosine theorem with vector?
I want to prove the cosine theorem of triangles with vectors under the following assumptions:
...
- 1,943
19
votes
1
answer
438
views
Programming language prototyping in Mathematica
Are you aware of any projects using the Wolfram language resp. Mathematica as an environment to explore the design of programming languages - in particular languages with a focus on mathematics (...
- 467
3
votes
0
answers
333
views
Can Mathematica be used as a proof assistant?
Mathematica have an extensive gallery of mathematical results, as well as a strong rule-based deduction system. Since v12.*, automated proving features have been added to it too.
I believe for ...
- 812
3
votes
1
answer
167
views
Axiomatizing naturals
Trying to implement the naturals in Mathematica, I follow E. Mendelson, Introduction to Mathematical Logic, Ch. 3, Par. 1.
Here is my code for the axioms (exept the induction axiom)
...
- 24k
2
votes
1
answer
110
views
How to deduce circle theorems in Wolfram language?
I can deduce the first one by applying FindGeometricConjectures on the following scene:
...
- 9,113
-2
votes
1
answer
137
views
Proving an integral identity [closed]
Assuming $f$ is continus on $[0,\pi]$, show that
$$\int_{0}^{\pi }xf(\sin x)dx=\frac{\pi }{2}\int_{0}^{\pi }f(\sin x)dx$$
I tried to demonstrate it using integration by parts, but I did not succeed.
...
- 195
1
vote
1
answer
130
views
Counting real roots of bivariate polynomial
For a proof, I'm working with a polynomial $p(x,m)$ and I need to show that: For any $m\in (0,6)$, $p_m(x)\equiv p(x,m)$ has a unique real root in $(0,1/2)$. I find that this is true by using Reduce ...
- 53
2
votes
0
answers
219
views
Natural deduction with FindEquationalProof
Out of curiosity, I'm trying to implement a natural deduction prover in Mathematica using FindEquationalProof. So far, I've implemented a few of the easier rules:
<...
- 988
7
votes
1
answer
216
views
Using logical equivalence to prove PL statements
I'm trying to use those Logical equivalence as axioms to prove some PL statements,
In this case I followed the examples in the documentation that didn't use the build-in logic functions$\{\text{And}[,]...
- 225
7
votes
3
answers
1k
views
Basic theorem proving in Mathematica?
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 ...
- 919
6
votes
1
answer
157
views
FindEquationalProof to prove divisor theorem
I'm trying to implement proofs of concepts for Equational Proofs on some basic number theory theorems.
One such example is:
"let a and b be positive integers and let d = gcd (a, b). If t divides ...
0
votes
1
answer
391
views
Implicit Function Theorem
I think I am stuck here right now:
The exercise is to use implicit differentiation to determine y' considering the following equation:
I managed to do this with:
...
- 3
4
votes
0
answers
89
views
Four color theorem in Mathematica [closed]
The four color theorem is a theorem about graphs (as in graphs and networks) and it was proved with the aid of a computer. To date, there is no hand-checkable proof. The software that was used to ...
- 627
2
votes
0
answers
141
views
FindEquationalProof with implications
Motivated by this question in mathematics, my Mathematica question is essentially this one, but alas the answer to that isn't quite adequate. I'm not interested in verifying that a proof is valid or ...
- 39.9k
7
votes
1
answer
424
views
FindEquationalProof with Logic in Wolfram Mathematica
I try to "make" proof in Wolfram Mathematica.
Thats a proof:
if a->b and b->c then a->c
I tried
...
- 71
6
votes
3
answers
400
views
Why Can't Mathematica Resolve this Simple Quantified Expression?
I've been using Mathematica as a hobbyist, off and on, for some time. So while I'm by no means an expert I've used it long enough to know that what might seem obvious to me is not necessarily obvious ...
- 71
5
votes
1
answer
246
views
Implementing the field axioms with FindEquationalProof?
I am fiddling around with FindEquationalProof, currently trying to prove some basic statements for fields. I have a set of axioms which almost constitutes the field theory axioms:
...
- 857
9
votes
1
answer
213
views
Proving uniqueness of group identity element
Start, as in the Mathematica 11.3 documentation, with:
...
- 11.8k
11
votes
2
answers
267
views
Clues on theorem proving tools?
I'm trying to prove $[a \cup (b \cap c ) = (a\cup b)\cap (a\cup c)]$ with Mathematica. But I don't know what function I should use. I've rewritten the sentence in the following way:
...
- 5,121
10
votes
4
answers
2k
views
How can I calculate the limit without using L'Hôpital's rule
I need to prove this limit without using L'Hôpital's rule:
$$\lim_{x\to 0} \frac{(1+a\,x)^{1/4} - (1+b\,x)^{1/4}}{x} = \frac{a-b}{4}$$
How can I do it in Mathematica?
- 111