Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [theorem-provers]

Automatic proof checkers verify the validity of formal proofs, while proof assistants aid in the construction of formal proofs. Some popular systems: Mizar, Coq, Isabelle. For automated theorem provers use the (automated-theorem-proving) tag

0
votes
1answer
31 views

How to Prove The Complement Of The Domain Is Complement Of The Image If f Is Bijective

It seems true that $f(\overline{X}) = \overline{f(X)}$ for $f:A\rightarrow B$ and $X$ is any subset of $A$ if and only if $f$ is bijective.But I couldn't write it as a formal way like epsilon argument....
4
votes
0answers
72 views

How does one prove that a computational theorem prover is correct?

There are many computational theorem provers, such as Z3 (http://z3.codeplex.com/). Such provers employ many thousands of lines of code. How can one prove that the results are correct and can be ...
3
votes
0answers
132 views

Can I use Coq to formalise the proofs from Terence Tao's Real Analysis textbook?

I'm working through Terence Tao's Real Analysis textbooks which start from Peano's axioms and build up from there and I was wondering can I use Coq to formalise and verify my proofs but without having ...
2
votes
0answers
44 views

Isabelle/HOL sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont

I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/...
1
vote
0answers
262 views

Coq transparency issues with type class fields

I am having some issues with, I suspect, transparency of fields in type classes. Consider a type class such as ...
0
votes
0answers
12 views

Prove that $q_A = {q_l}^2$ in geometric series of areas and corresponding side lengths of equilateral figures

Let $l_n$ be a geometric series of the side lengths of any equilateral two-dimensional figure and $A_n$ be a geometric series of the area of the said figure. Prove that $q_A = {q_l}^2$, whereas $q_A ...