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
47 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
65 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 ...
3
votes
0answers
55 views

Using an automatic tool for checking geometric conjectures

I do a lot of research about squares, and I thought of using some automatic tool for proving / disproving some geometric conjectures. As a simple example, consider the following Square coloring ...
2
votes
0answers
46 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
56 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
73 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
48 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
217 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
37 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 ...