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

Filter by
Sorted by
Tagged with
0
votes
0answers
12 views

Proving absolute maxima and minima of a bounded region given a condition (no Lagrange Method)

The following is a method to find the maxima/minima of a given boundary point problem. It should work for ay dimension. My question is, is my method correct? Please give me feedback as a comment on ...
0
votes
1answer
29 views

lean prover for $\neg (p \wedge \neg p)$

I did this code : section variable p : Prop example : ¬ (p ∧ ¬ p) := assume h : p ∧ ¬ p, show false, from (and.left h) (and.right h) end But I ...
-4
votes
2answers
87 views

Prove $(p → (q → r)) ↔ ((p ∧ q) → r)$ with lean4 [closed]

I try to solve the examples from chapter for from the online guide while learning lean4. But I can't solve this one. I'm as far as: ...
-1
votes
1answer
62 views

Proving diagonalization and inreversibility in matrices [closed]

I'm trying to prove two statements related to matrices but I can't find a good way to prove it: $$ T:R^{2}\rightarrow R^{2} $$$$ S:R^{2}\rightarrow R^{2} $$ Are linear transformations. What is the ...
0
votes
0answers
32 views

question about flooring a certain kind of numbers [duplicate]

Our math teacher was teaching us about the floor function and after finishing all the important parts we started to do some exercises by ourselves and there was this problem which we all did wrong: $$\...
0
votes
0answers
26 views

meaning of “modulo” in Formal Methods.

related to this question What is meaning of modulo specifically in the context of Tamarin prover: "Proofs are constructed using backward search with support for reasoning modulo equational ...
5
votes
1answer
94 views

Why are let binders part of the kernel in Coq/Lean?

I've been looking into the implementations of CIC-based theorem provers - mainly Coq and Lean - and it seems that both of them have let binders as part of the kernel, with their own typing and ...
-1
votes
1answer
97 views

On pairwise coprime $a_1,\ldots,a_n$ with $1<a_1<\ldots<a_n<(2n-1)^2$ [closed]

Given natural numbers $a_1, a_2, ..., a_n$ with $n$ coprime pairs. If it is known that the inequality $1 <a_1 <a_2 <... <a_n <(2n - 1) ^ 2$ is valid, prove that at least one prime ...
-1
votes
1answer
68 views

How to prove $\tanh^{-1}(\sin x)=\sin^{-1}(\tan x)$ [closed]

Here's what I attempted: $$ y =\tanh^{-1}(\sin x)$$ $$\tanh y=\sin x$$ But I don't know what to do after this. Please help me.
-2
votes
2answers
52 views

Prove that $|x|\le a$ [closed]

How can I prove this? $|x|\le a$, $\space \space$ $\:-a\le x\le a\:, $ $\space \space$ $a\in\mathbb{R}$. Thanks!
1
vote
1answer
29 views

Are there two norms in any space that neither of them is subordinate to the other?

Can you prove if no or give an example if yes? Obviously, this should be an example of an infinite-dimensional space, since in a finite-dimensional space, any two norms are equivalent.
1
vote
1answer
233 views

Proving first order logic in coq

I want to prove something like: Theorem new_theorem : $\forall (A B: \text{Prop}), ((A \wedge B) \iff (B \wedge A))$. in coq. I know, i could just type firstorder., but could i prove this in coq ...
0
votes
2answers
82 views

proving that $\sum_{k=0}^{n}{{n \choose k}{n+k \choose k}}=\sum_{k=0}^{n}{2^k{n \choose k}^2}$ [closed]

proving that $$\sum_{k=0}^{n}{{n \choose k}{n+k \choose k}}=\sum_{k=0}^{n}{2^k{n \choose k}^2}$$ (prove can be combi or algebraic)
1
vote
1answer
203 views

Translating "John is an adult man" into First Order Logic and Prover9 input [closed]

I am working on translating a really simple English statement into First Order Logic, which is- "John is an adult man" My first order logic axioms are the following- ...
-1
votes
2answers
34 views

How to prove a formula for the midpoint of a line between two vectors

how to prove that OP1 + 0,5 * P1P2 = OC? C is the midpoint of P1P2. Thank you Click here for the image that illustrates the problem
0
votes
1answer
98 views

DISPROVING "Every odd positive integer is the sum of a prime number and twice the square of an integer"

Providing a counter-example is enough to disprove a statement. However, it is not the only we of disproving. For example, if the statement is "$\sqrt{2}$ is a rational number", then we can disprove it ...
1
vote
0answers
50 views

"modulo" meaning in context of Formal Methods.

I am a beginner in the field of Formal Methods in Computer Science. In the literature, I often encounter phrases, such as "... modulo equation theory". Example are: SMT solver -- "Satisfiability ...
1
vote
0answers
42 views

Asking help with Riemann Integration [duplicate]

i need help with this theoretical exercise with Riemann integration, hope you can help me. Thanks. Prove that if $f:\mathbb{R}\rightarrow\mathbb{R}$ is continuous $\vert f\vert$ Riemann integrable ...
2
votes
2answers
242 views

Prove cycling in a Rubik's cube

How can I prove that if you apply some algorithm over and over again on a solved Rubik's cube, the cube will be solved? I mean mathematically not conceptually.
1
vote
0answers
58 views

The take lemma needs a coinductive proof

In Are coinductive proofs necessary?, the answerer claimed that we cannot prove inductively the take lemma: Two streams that agree on all initial subsequences of given length are the same. I was ...
0
votes
1answer
47 views

Prove: T$_1$ = T$_2$

If (X,T$_1$), (X,T$_2$) are compact and Hausdorff for T$_1$ and T$_2$ which are comparable prove T$_1$ = T$_2$. Well my idea was to create a function F between (X,T$_1$) and (X,T$_2$) that carry one ...
1
vote
0answers
67 views

How to prove $r \implies (\exists x : \alpha, r)$ in Lean

I'm trying to prove the logical statement $r \implies (\exists x: \alpha, r)$, where $r$ is a Prop (a proposition or statement) and $\alpha$ is a ...
-4
votes
3answers
658 views

prove that if $m$ and $n$ are integers and $m+n$ is odd then $m-n$ is odd. [closed]

prove that if m and n are integers and m+n is odd then m-n is odd.
-2
votes
1answer
75 views

Prove $xy\leq \frac{x^p}{p} + \frac{y^q}{q}$

Let $p,q>1,\ \frac1p+\frac1q=1$, and $x,y>0$. Prove that $xy\leq \frac{x^p}{p} + \frac{y^q}{q}$ by using natural log, definition of concave function, and the fact that natural log is a concave ...
0
votes
2answers
42 views

How to prove this formula. Formula is for evaluate limits which answers are e to the power something.

I would like to ask you about how to prove this formula. I come up with this formula when i was browsing internet. It works when i used it on given examples, but i would like to know if it works in ...
0
votes
2answers
37 views

formal definition prove for $\lim_{a \to \infty} \{a_n\} = a$ also applies to $\{-a_n\} \to -a$

By definition of any sequence $\{a_n\}$: if $\lim_{n \to \infty} a_n$ = a, then for all values $\epsilon > 0$, there exists a value $N \in \mathbb{N}$ such that for all values $n > N$ then $|a_n ...
2
votes
4answers
64 views

Proving the equation using binomial theorem

I want to prove this theorem using Binomial theorem and I've got trouble in understanding 3rd step if anyone knows why please explain :) Prove that sum: $\sum_{r=0}^{k}\...
4
votes
1answer
291 views

Why typeclasses rather than inductive types to define mathematical structures in Lean?

I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik). In the Lean Prover mathlib library, typical mathematical ...
0
votes
1answer
26 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 ...
0
votes
0answers
152 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 ...
3
votes
3answers
55 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
160 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
46 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
0answers
391 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....
0
votes
2answers
314 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 ...
3
votes
1answer
138 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
144 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 ...
2
votes
1answer
260 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, ...
9
votes
1answer
815 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) ...
5
votes
0answers
191 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
2answers
499 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
50 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
145 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 ...
1
vote
2answers
222 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
2answers
132 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 ...
2
votes
1answer
88 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
226 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 ...
2
votes
1answer
190 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, ...
5
votes
0answers
86 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 ...
11
votes
1answer
443 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 ...