Questions tagged [theorem-proving]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 ...
ShyPerson's user avatar
  • 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$
Rebel's user avatar
  • 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?
hengxin's user avatar
  • 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: ...
Alex's user avatar
  • 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 ...
Jason Turner's user avatar
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$ (...
David G. Stork's user avatar
1 vote
0 answers
122 views

What should be the response of FindEquationalProof?

The code ...
user64494's user avatar
  • 24k
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 ...
David G. Stork's user avatar
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 ...
atat's user avatar
  • 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 ...
Carlo Beenakker's user avatar
1 vote
2 answers
178 views

Finding a root that makes this huge polynomial negative

I have the following polynomial. ...
Morcus's user avatar
  • 247
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: ...
mrz's user avatar
  • 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: <...
lotus2019's user avatar
  • 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: ...
lotus2019's user avatar
  • 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 (...
Math Gaudium's user avatar
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 ...
Gravifer's user avatar
  • 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) ...
user64494's user avatar
  • 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: ...
user13892's user avatar
  • 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. ...
Huanca Sullca's user avatar
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 ...
ilan's user avatar
  • 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: <...
imas145's user avatar
  • 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}[,]...
Ethan's user avatar
  • 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 ...
dharmatech's user avatar
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 ...
Ten-Thousand-Hands's user avatar
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: ...
stefan's user avatar
  • 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 ...
EGME's user avatar
  • 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 ...
David G. Stork's user avatar
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 ...
J.A.B.'s user avatar
  • 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 ...
Ben Hekster's user avatar
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: ...
Michael L.'s user avatar
9 votes
1 answer
213 views

Proving uniqueness of group identity element

Start, as in the Mathematica 11.3 documentation, with: ...
murray's user avatar
  • 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: ...
Red Banana's user avatar
  • 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?
Black Marik's user avatar