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

3
votes
3answers
51 views

Prove of a theorem of a geometrical place

I am having issues to prove the back of this theorem: Let $ABC$ be a triangle and fixed $D∈AB$. The Geometric Place of the $X$-points that form with $D$ and an arbitrary point $S∈AC$ an ...
1
vote
1answer
61 views

predecessor and multiplication prove

I have trouble, when attempting to : 1- prove mult defines the multiplication function. 2- Prove pred defines the predecessor function. 1- for mult: Base Case: mult 0x= 0 Inductive case: := $(\...
0
votes
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 ...
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....
7
votes
3answers
617 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 ...
0
votes
2answers
62 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 ...
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 ...
3
votes
1answer
86 views

Sharkovsky's theorem, period 4 implies period 2

I need to prove that using the ordering of the Sharkocsky's, that period 4 implies period 2. Thus for a continuous function f from the unit interval to the unit interval itself, I need to prove that $...
2
votes
3answers
116 views

Combinatorics sum to 1 using Identity

I want to prove that the following equals 1: $W=\sum_{i=0}^{n-r}(-1)^i n \frac{C_{n-1}^{r-1}C_{n-r}^i}{(r+i)}$. I tried mathematical induction and succeeded. Is there any known identity of ...
1
vote
1answer
139 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, ...
3
votes
1answer
300 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) ...
2
votes
2answers
98 views

Peano/Presburger axioms - “find” numbers lower or equal than another number

[EDIT/CONCLUSION] It turns out it was actually working.. I was just like too stupid to let the prover run for more time and assumed it would take a lot / not be able to prove with what I've provided ...
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 ...
0
votes
1answer
218 views

Simple LTL formulas into First Order Logic formulas

I would like to know if it is possible to transform simple LTL logic formula i.e.: $G a$ or $F a$ (where $G$ - globally, $F$ - finally) to First Order Logic formula. I was wondering if the below ...
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/...
0
votes
1answer
100 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 ...
8
votes
1answer
335 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 ...
1
vote
2answers
133 views

First Order Logic Inference , Proof of sentence

I need to find a proof for my goal , given some assumptions. The assumptions and the goal were translated from english sentences. My assumptions(KB) John ,Mary,Helen,George are the only members of ...
2
votes
1answer
59 views

Is there any mathematical work on formalizing problems and their solutions as mathematical objects?

Problems (tasks?) are an important part of life, science, math, basically everything. Do people study them as mathematical objects? Theorem proving seems close, however, I'm interested more in the ...
0
votes
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 ...
11
votes
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 ...
2
votes
1answer
182 views

An endless loop in a program that search for mathematical theorems and proofs − a milestone? [closed]

I don't know if there exist computer programs working on its own, trying to find and prove theorems, delivering proofs and go on searching for new theorems. But if (when) there are such programs, ...
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
2answers
848 views

Automatic theorem prover for proving simple theorems?

Is there a simple software that I could use to practice proving theorems in my course of mathematical logic? Basically what I need is ability to 1) define what axioms and laws I am allowed to use in ...
3
votes
1answer
176 views

Why is automated proof checking so hard?

(Warn: this is not about automated proving which is impossible. It is about the automatized proof checking). For example, there is no automated test developed for Wiles Theorem (aka Fermat last ...
8
votes
1answer
286 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 ...
5
votes
1answer
321 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 ...
0
votes
2answers
65 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 ...
25
votes
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 ...
0
votes
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 ...
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 ...