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

learn more… | top users | synonyms

0
votes
0answers
23 views

Searching an on-line tableau prover for FOL

I am searching for an online prover that proves first-order logic (FOL) formulas or sequents. I want that the prover is based on a tableaux method that displays proof trees. Dealing with FOL with ...
1
vote
0answers
14 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 ...
0
votes
1answer
16 views

Lining a rectangular building square panels

I've been working on this for what feels like a lifetime now and I'm just not getting anywhere with it. I'm wondering if someone would be able to explain how to solve it for me? There is a ...
2
votes
3answers
45 views

How can I prove that the square of an even number ends in 0/4/6?

I am trying to prove that the last digit of the square of an even number is either 0, 4, or 6 but I'm completely lost and have no idea how to tackle this problem.
0
votes
0answers
8 views

Are there tools for presentation and vizualization of deduction?

I read that Kalish and Montague introduced a natural deduction method (http://en.wikipedia.org/wiki/Donald_Kalish), which can be easily implemented in software. Any other tools who can help a logician ...
1
vote
1answer
18 views

Random conversions

I came across a question in StackOverflow which states the following, all is based on natural numbers: Given the function rand5 (which produces random natural numbers 0-4), use it to generate a rand7 ...
1
vote
1answer
53 views

Prove that $\frac {1}{a_1a_2} + \frac {1}{a_2a_3} + \frac {1}{a_3a_4} + … + \frac {1}{a_{n-1}a_n} = \frac {n-1}{a_1a_n}$

There is this question in one of my math textbooks which i can't seem to figure out how to solve, it'd be awesome if you could help me : If $a_1,a_2,a_3,...,a_n$ IS an arithmetic progression and ...
0
votes
2answers
49 views

Is this trigonometric identity correct?I tried by using compound formulae for cos8A but …

Prove that: $\sqrt{2+\sqrt{2+\sqrt{2\cos(8A)}}}=2\cos A$ Is this trigonometric identity correct?, I tried by using compound formulae for cos8A but couldn’t get it to RHS, give your try and if ...
1
vote
1answer
41 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 ...
2
votes
1answer
83 views

Proving the propositional tableau sound and complete

There is something fundamental that stops me from understanding the proofs for the propositional tableau. (1) soundness proves that all theorems that can be proved are valid (2) completeness proves ...
0
votes
0answers
31 views

How to handle “positive difference or zero”?

Particularly in the type $\mathtt{nat}$ within the proof assistant Coq, I encounter an operation on nonnegative integers that we can define as $d(m, n) = \max(0, m - n)$. I think that without ...
5
votes
1answer
181 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
1answer
52 views

Help me prove this principle with other Hilbert system principles

I have two choices: 1.to show that this principle is correct with other Hilbert system principles the first order $\forall x(A \to B(x)) \to (A \to \forall x B(x))$ (original screenshot) OR 2. to ...
2
votes
2answers
177 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 ...
0
votes
2answers
48 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 ...
1
vote
3answers
2k views

Prove « If P(A) is a subset of P(B) => A is a subset of B » [duplicate]

I need to prove «If P(A) is a subset of P(B) => A is a subset of B», generally, I understand the main way I should prove it, but the problem is in formal, pedantic language I have to use to prove ...
1
vote
2answers
166 views

“Points E and F lie on the sides BC and CD rectangle ABCD, the AEF is an equilateral triangle”

Points E and F lie on the sides BC and CD of rectangle ABCD, the AEF is an equilateral triangle. M is the midpoint of the AF. Prove that the triangle BCM is equilateral .
6
votes
2answers
197 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 ...
6
votes
3answers
337 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 ...
0
votes
1answer
96 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 ...
7
votes
1answer
195 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 ...
1
vote
0answers
204 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 ...
21
votes
3answers
763 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 ...