Tagged Questions

The tag has no wiki summary.

learn more… | top users | synonyms

4
votes
2answers
49 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
2answers
103 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?
13
votes
1answer
202 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
44 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
40 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?] ...
1
vote
1answer
62 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
375 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
51 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
48 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
61 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
0answers
47 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 ...
1
vote
2answers
164 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
63 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 ...
5
votes
2answers
172 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 ...
2
votes
2answers
120 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
65 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
129 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
92 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 ...
6
votes
2answers
465 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, ...
2
votes
1answer
213 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 ...
4
votes
3answers
300 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
66 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 ...
14
votes
6answers
702 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 ...
37
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
83 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
47 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
60 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 ...
6
votes
4answers
481 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
87 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?
0
votes
2answers
226 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
203 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
187 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
440 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 ...