Questions tagged [theorem-proving]
The theorem-proving tag has no usage guidance.
11
questions
5
votes
1answer
137 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}[,]...
5
votes
1answer
146 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 ...
2
votes
0answers
38 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
1answer
108 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
0answers
59 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 ...
1
vote
0answers
66 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 ...
5
votes
1answer
160 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
...
5
votes
3answers
171 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
1answer
139 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
1answer
144 views
Proving uniqueness of group identity element
Start, as in the Mathematica 11.3 documentation, with:
...
8
votes
1answer
168 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:
...
