# Questions tagged [theorem-proving]

The tag has no usage guidance.

33 questions
Filter by
Sorted by
Tagged with
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 ...
1 vote
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$
1 vote
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?
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: ...
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 ...
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$ (...
1 vote
122 views

The code ...
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 ...
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 ...
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 ...
1 vote
178 views

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

I have the following polynomial. ...
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: ...
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: <...
96 views

### How to deduce cosine theorem with vector?

I want to prove the cosine theorem of triangles with vectors under the following assumptions: ...
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 (...
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 ...
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) ...
110 views

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

I can deduce the first one by applying FindGeometricConjectures on the following scene: ...
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. ...
1 vote
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 ...
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: <...
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}[,]... 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 ... 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: ... 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 ... 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 ... 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 ... 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 ... 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: ... 9 votes 1 answer 213 views ### Proving uniqueness of group identity element Start, as in the Mathematica 11.3 documentation, with: ... 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: ...
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?