# Questions tagged [theorem-proving]

The tag has no usage guidance.

19 questions
Filter by
Sorted by
Tagged with
57 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 ...
22 views

### Clarifying the syntax of FindEquationalProof

Could someone clarify the definitions of "statement" and "expression" in the manual entry for FindEquationalProof? The best I can make of it is that an expression $E$ is either a ...
112 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) ...
76 views

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

I can deduce the first one by applying FindGeometricConjectures on the following scene: ...
122 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. ...
74 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 ...
69 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}[,]... 3answers 459 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 ... 1answer 100 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 ... 1answer 248 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: ... 0answers 70 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 ... 0answers 89 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 ... 1answer 266 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 ... 3answers 264 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 ... 1answer 185 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: ... 1answer 171 views ### Proving uniqueness of group identity element Start, as in the Mathematica 11.3 documentation, with: ... 2answers 223 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?