For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

learn more… | top users | synonyms

2
votes
1answer
55 views

define the “optimal” automatic theorem prover

my question is : is it possible to define in some way what should do an "optimal automatic mathematician" ? There are two points of view of an automatic theorem prover / automatic mathematician : ...
5
votes
0answers
66 views

An Auto-Generated Cartography of Mathematical Theories: Has it been done already?

While looking for a way to visualize the logical structure of mathematical theories a graph-like depiction came to my mind, where propositions are represented by vertices. An edge goes from ...
2
votes
0answers
48 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 ...
2
votes
0answers
57 views

Is it useful to learn to use automatic theorem provers?

I mean, do ATP's spot some obvious errors in computations or proofs? And if I'm not sure about the correctness of some modern proof found in some article, say for example Mochizuki's proof of the ABC ...
2
votes
0answers
87 views

Ordering of multisets in “Paramodulation based theorem proving”

I'm reading this paper: http://www.lsi.upc.edu/~albert/papers/handbook.ps.gz and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A ...
1
vote
0answers
74 views

Proving irregularity using Myhill-Nerode theorem

I'm trying to prove that the following language is irregular using the Myhill-Nerode theorem $$ L = \{ w\space\epsilon \{a,b,c\}^* | \#_b(w) > (\#_a(w) + \#_c(w))! \} $$ While it's completely ...
1
vote
0answers
86 views

A question about a projection of a variety

Let $\mathbb K$ be an algebraically closed field (of characteristic zero) and $H$ an irreducible variety in $\mathbb K ^n$. Let $t \in \mathbb K [x_1,\ldots,x_n]$ and let $T:= \mathsf V ( t )$ be the ...
1
vote
0answers
49 views

Cone relations and equivalence relations in the Myhill - Nerode Theorem.

Fix an alphabet ${\bf S}$ and a language $L \subset S^*$. For any two words $w$, $w'$ $\in S^*$, define a relation $w \sim w'$ if and only if Cone$(w)$ = Cone$(w')$. Then prove that this is an ...
1
vote
0answers
218 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 ...
0
votes
0answers
39 views

Computer verification of Fermat's Last Theorem - status

My question is about the status of proof verification...and specifically about Fermat's last theorem. How close are we to having computers able to verify theorems of this complexity. What about the ...