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

60 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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: ...
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 ...
32 views

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....
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 ...
138 views

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/...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...