Questions tagged [theorem-proving]

The tag has no usage guidance.

4 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
2
votes
0answers
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: <...
1
vote
0answers
58 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 ...
1
vote
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 ...
0
votes
0answers
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 ...