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

1
vote
1answer
46 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 ...
0
votes
1answer
16 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, ...
1
vote
3answers
101 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 ...
-1
votes
1answer
35 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 ...
3
votes
2answers
97 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' ...
3
votes
1answer
73 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 : ...
6
votes
1answer
76 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 ...
2
votes
1answer
140 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, ...
1
vote
1answer
104 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 ...
2
votes
0answers
72 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 ...
4
votes
2answers
111 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 ...
3
votes
1answer
70 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 ...
4
votes
2answers
89 views

When is de-Skolemizing statements appropriate?

In first order logic we often convert prenex normal form statements to Skolem normal form statements to eliminate the existential quantifier: $\exists$x$\forall$y$\exists$z$\phi$(x,y,z) becomes ...
1
vote
1answer
134 views

An impressive fact expressible in presburger arithmetic?

Is there something expressible in presburger arithmetic that would seem impressive to students at an undergraduate level?
15
votes
1answer
385 views

Rings with $a^5=a$ are commutative

Let $R$ be a ring such that $a^5=a$ for all $a \in R$. Then it follows that $R$ is commutative. This is part of a more general well-known theorem by Jacobson for arbitrary exponents ($a^n=a$), which ...
2
votes
0answers
61 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 ...
1
vote
1answer
190 views

A simple, yet non-superficial explanation of what “paramodulation” means in the context of automated theorem proving?

Modern automated theorem provers seem to be paramodulation-based. I only have a superficial understanding of what this means: we derive a proposition whose truth is implied from the truth of [two?] ...
2
votes
1answer
132 views

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
8
votes
4answers
437 views

Why isn't math completely solved by expert systems? [duplicate]

Everything in math can be perfectly defined or formalized. And we could derive logical conclusions from that. However, mathematicians still use human natural language to solve their theorems. Why ...
1
vote
0answers
90 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
2answers
79 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 ...
0
votes
1answer
80 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 ...
3
votes
1answer
68 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
2answers
257 views

Automatic theorem prover for proving simple theorems?

Is there a simple software that I could use to practice proving theorems in my course of mathematical logic? Basically what I need is ability to 1) define what axioms and laws I am allowed to use in ...
5
votes
0answers
73 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 ...
6
votes
2answers
304 views

natural language proof assistant

I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english, I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then ...
3
votes
2answers
131 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 ...
1
vote
0answers
99 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 ...
2
votes
1answer
136 views

Equivalent statements

If one looks at the directed graph of all theorems proved, let there be a vertex between statement A and B directional if A implies B, ideally it will connect results across different fields. Is there ...
3
votes
1answer
125 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 ...
9
votes
2answers
786 views

Could computers someday discover theorems or find demonstrations?

Cloud computing and quantum computers bring computers to what seems like a limitless calculation power? If one sees all the mathematical operations and theorems as a toolset that a computer can use, ...
3
votes
1answer
288 views

Inequalities of quotients of elementary symmetric polynomials

Many inequalities regarding symmetric polynomials such as this are posed as problems http://www.artofproblemsolving.com/Wiki/index.php/1997_USAMO_Problems/Problem_5 ...
5
votes
3answers
332 views

In a monoid, does $x \cdot y=e$ imply $y \cdot x=e$?

A monoid is a set $S$ together with a binary operation $\cdot:S \times S \rightarrow S$ such that: The binary operation $\cdot$ is associative, that is, $(a\cdot b) \cdot c=a\cdot (b \cdot c)$ for ...
1
vote
1answer
67 views

Knuth-Bendix ordering and the one unary function

I'm looking at Knuth-Bendix ordering in the context of theorem proving with the superposition calculus. The explanations of KBO that I've been able to find say among other things that each function ...
16
votes
6answers
853 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 ...
41
votes
6answers
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 ...
2
votes
0answers
94 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
52 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 ...
0
votes
1answer
64 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 ...
9
votes
4answers
849 views

How to start with automated theorem proving?

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 ...
1
vote
1answer
96 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?
-1
votes
2answers
235 views

Idea: Resource to avoid publishing something someone else published [closed]

Researchers often prove theorems but they don't know whether somebody else already published the same result. One strategy is to read papers on the topic or search keywords, however it would take way ...
1
vote
0answers
225 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 ...
2
votes
1answer
252 views

Superposition calculus and equality factoring

Superposition with equality resolution and equality factoring is said to be a complete calculus for first-order logic. The purpose of equality factoring is basically to get rid of paraduplicate ...
17
votes
2answers
503 views

Is there an automated way to prove really boring elementary number theoretic results?

Motivation: I'm writing a proof, and within it, I need to prove: Conjecture: Let $p$ be an odd prime (i.e. $p \neq 2$). Let $c \geq 2$, $d \geq 1$ and $r \geq 1$. If $p^r$ divides $cd$, then ...