# 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
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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) ...
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 ...
98 views

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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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....
12 views