# Tagged Questions

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

67 views

### Could mathematical reasoning be non-axiomatic?

"Mathematics is not a deductive science—that's a cliché. When you try to prove a theorem, you don't just list the hypotheses, and then start to reason. What you do is trial and error, experimentation, ...
58 views

### If finitely many algebraic identities do not imply some identity, is there always a finite counterexample?

This question just popped up while experimenting with Prover9 and Mace4. Say we have a finite signature and some finite set of identities $E_i$ in the sense of universal algebra, like the axioms for ...
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 ...
25 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: ...
56 views

### Is this a well defined problem in terms of Euclidean Geometry?

I am trying to construct an example of a geometric problem, stated in terms of Euclidean Geometry, that is not Machine Provable (or in an equivalent definition Automatically Provable)-i.e no computer ...
59 views

### Deductive logic counter-intuitive result

I am working on a small proof in deductive logic. Here is what must be proved: $(\exists x \in T \mid A \implies P(x)) \implies A \implies (\forall x \in T \mid P(x))$ To me that looks unprovable ...
51 views

### From a set of rules, derive the implications?

I've only just become interested in this domain, so sorry if I'm not using the correct terminologies. What I want is the following: Say I have a set of rules (or constraints), I want to derive some ...
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, ...
103 views

### Prime numbers qns

Show that for any prime number $p$, $q$, $r$, one has $p^2+q^2$ does not equal to $r^2$. I have no idea how to start and prove it. One stumbling part is that we cannot deduce with certainty that r ...
40 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 ...
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' ...
80 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 : ...
81 views

### Distance between theorems

In automated proving one can define the best proof of a theorem as the one which minimizes the length of the proof. Given a set of known statements one could define the difficulty of a theorem as the ...
145 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, ...
122 views

### Automata Language regularity proof by construction.

I've been trying to prove or disprove a question that popped during our last session in Uni, we've been using automaton constructing to prove regularity for a while now and I really do have the handle ...
94 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 ...
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 ...
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 ...
117 views

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

I'm interested in this question, but I'm not going to list my knowledge/demands but rather gear it to more general purpose; so the first thing concerns the prerequisites, i.e. How much ...
104 views

### Algorithm for enumerating theorems of first-order theories besides resolution

Is there a general algorithm for enumerating the theorems of any finite first-order theory with a better time complexity than simply using resolution on all first-order logic formulas?