# Tagged Questions

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

2k views

### Has any previously unknown result been proven by an automated theorem prover?

The Wikipedia page on automated theorem proving states: Despite these theoretical limits, in practice, theorem provers can solve many hard problems... However it is not clear whether these 'hard ...
907 views

### What are the theorems of mathematics proved by a computer so far?

By theorems, I mean the ones you can find in an undergraduate course of mathematics, not the ones you can find in a textbook of automated proofs. I mean by "proved by a computer" that an existing ...
522 views

136 views

### Algorithm to find a proof of every provable theorem.

I found this pdf while searching on automated theorem provers: https://www.math.ucdavis.edu/~greg/145/notproof.pdf It says: "Proof by rote algorithm Non-proof courses in mathematics generally ...
117 views

### Proofs about theorem-provers in ZFC, in ZFC

Is the following statement provable in ZFC for some $A$: "$A$ is an algorithm which, when given as input a proposition $p$ in the language of ZFC, outputs 'yes' only if $p$ is provable in ZFC, 'no' ...
135 views

### Would it be possible to concoct a “harmful” axiom?

Suppose I run an automated theorem prover. It begins with the axioms of ZFC, and using a random number generator, it proves more theorems, and it runs for two days. At the end of the second day, it ...
80 views

### Programming First-Order Logic

So I recently started reading about logic, and I have decided to try to implement the subject in my final project for a mathematical programming class I am taking. I wasn't going to try to make ...
141 views

### What does Equational Theorem Prover do?

http://www.cs.unm.edu/~mccune/eqp/ What does EQP do? Is there any paper that explains what it does? README and other read files do not provide such information - it only talks of how to use it and ...
69 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 ...
298 views

91 views

### How to construct NFAs that recognize the following languages.

I am new to this computation theory and I am trying to answer the following question. Can you please check if I am on the right track? If there is any material that I can study for problems like these,...
117 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 ...
53 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 ...
232 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 ...
94 views

### Some questions about strict tableau in propositional calculus (raising from a book by Melvin Fitting)

Recently, I encountered some questions when reading First-Order Logic and Automated Theorem Proving (1st ed - 1990), by Melvin Fitting. 1: confusing definition of strict tableau (page 39 definition ...
65 views

### Modelchecking on Automata, $\phi$ not SAT and $\phi \models$ False

Given a formula $\phi$ Is $\phi \models FALSE$ equivalent to $\phi$ not SAT? Or does $\phi \models FALSE$ means that $\phi$ is never $TRUE$ and $\phi$ not SAT means, that there existst at least one ...
40 views

### Constructive proof of pigeonhole principle as stated in Software Foundations book

I'm trying to prove the pigeonhole principle from Pierce et al. Software Foundations book and I'm stuck with trying to do so without use of the principle of excluded middle. Here Coq formulation of ...
24 views

### The right way of defining a predicate

My theory contains a definition of lists: L(H,T) is a list, H is the first element (head), T is the list of remaining elements (tail), nil is empty list. So [A,B,C] = L(A,L(B,L(C,nil))). I defined ...
39 views

### Unary predicate for finite number of values

I am working with automated prover. I am creating a theory, where an unary predicate PR should be true just for several constants, false otherwise. I made following axioms: ...
17 views

### Equivalence classes of $\{ij\ |\ i, j ∈ \{a, b\}^* , i \neq j\}$

I want to find the equivalence classes (Nerode-relation) of this language: $L = \{ij\ |\ i,j \in \{a,b\}^*,\ i \neq j\}$ It says that this language is regular and that it has 2 equivalence classes, ...