# 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

34 questions
3answers
2k views

### How do proof verifiers work?

I'm currently trying to understand the concepts and theory behind some of the common proof verifiers out there, but am not quite sure on the exact nature and construction of the sort of systems/proof ...
4answers
2k views

### Is it possible to prove everything in mathematics by theorem provers such as Coq?

Coq has been used to provide formal proofs to the Four Colour theorem, the Feit–Thompson theorem, and I'm sure many more. I was wondering - is there anything that can't be proved in theorem provers ...
1answer
342 views

### Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order ...
1answer
290 views

### Are coinductive proofs necessary?

I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
3answers
619 views

### natural language proof assistant

I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english, I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then ...
1answer
323 views

### Proving that e.g. 421 is prime in a formal system

I'm working in the formal system Metamath, and in the course of learning about number theory I've become acquainted with theorems, such as Bertrand's postulate, that require hand-calculation that a ...
1answer
317 views

### Getting to know the Mizar Mathematical Library

I want to do some formalization of mathematics using Mizar. From their Bibliography site I've read "Writing a Mizar article in nine easy steps" by F. Wiedijk (very good for the basic understanding) ...
0answers
73 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 ...
1answer
98 views

1answer
160 views

### First Order Logic knowledge base problem

I would like to present in the predicate logic the knowledge base and then check if the one provided formula is satisfied using the defined knowledgebase. I am trying to do this using SPASS prover, ...
0answers
264 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 ...
1answer
138 views

### Why do we need tactics, reflection and other techniques when we have Curry-Howard for theorem proving?

First of all, I apologize if this question is slightly misplaced, but this seemed the best place to ask it given the mathematical/theoretical nature of the discussion. Given that the Curry-Howard ...
1answer
35 views

### Is it sufficient to prove $P(x) \geq a$ if we already know $P(x) > a$?

Is it sufficient to prove $P(x) \ge (\text{or} \le) a$ if we already know $P(x) > (\text{or} <)a$? For example, to prove $$\forall n \ge 1 , \sum_{i=1}^{n}\frac{1}{i^2} \le 2$$ Suppose I ...
2answers
79 views

### How to prove that the XOR problem for dimension d is not lineary seperable

The 2 dimensions xor problem can be converted to 4 equations which is possible to prove that are not possible to solve ...
1answer
106 views

### Interactive proof assistants (IPA) and automated theorem provers (ATP) for analysis and variational calculus?

Is it possible to use (and how) interactive proof assistants (like Isabelle/HOL, Coq) and automated theorem provers (like E) for proving theorems in analysis and variational calculus and solving ...
2answers
66 views

### Why this first-order logic formula is not correct?

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover. I'm having some problems formalizing this: "John, Mary and Derek are three ...
1answer
22 views

### Prove: $\forall x ( R(x,x) \to R(a,a))$

Nãoconsigo entender como se prova este argumento, podem me ajudar: $\forall x ( R(x,x) \to R(a,a))$ Translation: I don't understand how to prove that $$\forall x ( R(x,x) \to R(a,a))$$ Could you ...
0answers
22 views

### Cosets form a group if normal subgroup [duplicate]

Given a group G and its subgroup H that creates cosets, prove that cosets form a group iff H - is a normal subgroup. I've tried to find any good prove but I failed - most of the sources (including ...
1answer
35 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....
0answers
12 views

1answer
137 views

### Help with Prover9 for weak propositional systems

I am trying to get Prover9 to work, but apparently am not using exactly the correct commands. Can someone give me a hint, please? This is just a test case, but ...
8answers
64 views

### How do I prove that the sum of any integer ≥ 1 and its square will always result in an even number? [closed]

I started with x + x^2 = 2n but got nowhere