Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [automated-theorem-proving]

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

4
votes
1answer
124 views

Is there a theorem prover that works in natural language?

I'm interested in a computer program, possibly a web app, that could prove theorems and show its proofs. I essentially want to type in a theorem like "For every bounded sequence, there exists a ...
0
votes
1answer
33 views

Can any 1st-order proof be expressed with an SMT?

Is it possible to rephrase every proof which uses first-order logic into a proof which uses satisfiability modulo theories? In other words, can a program which automatically solves SMT questions solve ...
7
votes
0answers
84 views

Are “Discovery Systems” still not viable in mathematics?

I am currently reading Why did AM run out steam?, an article regarding Douglas Lenat's Automated Mathematician (AM). AM is an early example (from 1976) of a "discovery system" - a system that attempts ...
4
votes
2answers
297 views

Curry-Howard for an imperative programming language?

The Curry-Howard isomorphism links proofs of propositions, with "programs" and types. But the way I am introduced to it, "programs" is interpreted in a functional way, i.e. in lambda calculus with ...
1
vote
1answer
93 views

Can all classical math proofs be represented in type theory?

The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types. However, I'm wondering: if we add the classical logical axioms like LEM (and ...
1
vote
1answer
138 views

First Order Logic knowledge base problem

I would like to present in the predicate logic the knowledge base and then check if the one provided formula is satisfied using the defined knowledgebase. I am trying to do this using SPASS prover, ...
0
votes
1answer
80 views

Who to define the meta-function using induction prinicple?

I'm a beginner in Automated Theorem Proving, and I want to proof using the induction principle from the syntactic definition of propositional formulae, define the meta-function $V[\phi]$ which gives ...
2
votes
1answer
126 views

Transforming a formula into clausal form

I've been having some difficulty in transforming the following formula to a clausal form: $\forall x(biker(x) \to \exists y((harley(y) \lor bmw(y)) \land rides(x,y)))$ I've taken the following steps:...
0
votes
1answer
24 views

Problem with transforming a formula to Prenex CNF

I've been trying to transform the following formula all day long with no avail: $\lnot[\forall x \exists y F(u,x,y) \to \exists x (\lnot \forall y G(y,v) \to H(x))]$ the answer sheet gives us the ...
0
votes
1answer
33 views

Should $\to$-elimination always have precedence over $\lnot$-elimination when transforming formulas to Prenex CNF?

I'm currently learning the resolution method of proof and before it can be applied we need to transform a FOL formula into prenex, then skolemise it, then transform it to CNF, correct? I encountered a ...
0
votes
0answers
45 views

ZF-like set theory in HOL

I implemented a ZF-like set theory in PVS, a HOL-based theorem prover. The difference with ZF is that the replacement axiom scheme is formalized by an axiom with universal quantification over ...
29
votes
8answers
3k views

Why is there not a system for computer checking mathematical proofs yet (2018)? [closed]

As of 2018, mathematical proofs are still being decided by human consensus. i.e. Give the proof to a few capable humans and if none of them can find any errors than they vote that the proof is correct ...
4
votes
0answers
57 views

Automated proof verification of metalogical theorems of first order logic

Have any of the metalogical theorems of first order logic, such as the deduction theorem, been formalized and proven in a system such as Coq or HOL? If not, what are the main obstacles to doing so?
1
vote
0answers
68 views

Is type theory a required background to make an automated theorem prover?

There's a lot of theory involved in automated reasoning, but why not represent things with any old OOP hierarchy that makes sense? Do I need to learn another area of math to make something that ...
2
votes
1answer
208 views

What Progress Made in Automated Verification of Mathematical Proofs?

The problem was that these [automated proof verification] systems were extraordinarily cumbersome. Checking a single theorem could require a decade of work, because the computer essentially had to ...
-5
votes
3answers
469 views

Proving -(-a)=a Using Field Axioms [closed]

I can use only these given field axioms to prove the following expressions: $$ I. -(-x) = x $$ $$ II. ab=1 $$ A. The Property of Closure B. Commutative Property C. Associative Property D. Inverse ...
2
votes
3answers
133 views

A rigorous proof of ∀ m ∈ ℕ, 0 < m → 1 < 2 * m

There's a class of problems I struggle to prove by induction/recursion (I'm working in CIC). The best way I can describe this class of problems is "finite cases below m, inductive case above m". An "...
1
vote
0answers
70 views

Numbers made from digits 1-9 — proving the exceptions?

Inspired by this paper Introduction In this paper, a sequential representation of a number is a formula that uses the digits 1-9 in order with the mathematical operations +, -, ×, ÷, ^, as well as ...
1
vote
1answer
90 views

Question about proof verifiers like metamath.

How does metamath or other proof verifiers determine if two propositional formulas can be made equal? Pointers to the literature would be appreciated.
0
votes
1answer
99 views

Interactive proof assistants (IPA) and automated theorem provers (ATP) for analysis and variational calculus?

Is it possible to use (and how) interactive proof assistants (like Isabelle/HOL, Coq) and automated theorem provers (like E) for proving theorems in analysis and variational calculus and solving ...
0
votes
1answer
91 views

Understanding the useness of Classification of finite simple groups

I know that we are able to classify all the finite simple group, but I don't understand how to use this classification to prove results like that every simple group has two generators. The ...
1
vote
1answer
139 views

How Mathematica differs from proof assistants, i.e. is it possible to embedd logics in Mathematica?

How Mathematica differs from proof assistants? Specifically - proof assistants can be used for embedding/implementing logics into them, like "Working with Linear Logic in Coq" http://www.cs.nuim.ie/~...
4
votes
0answers
156 views

What mathematics cannot be done in proof assitants (Isabelle/HOL, HOL) and how proof assistants should be improved?

What mathematics cannot be done in proof assitants (Isabelle/HOL, HOL) and how proof assistants should be improved? I am working on the project of mechanizing algorithms in Isabelle/HOL and I would ...
0
votes
2answers
75 views

Want to clarify and check DFA and NFA attempt

I did following exercise and i want to clarify that did i made something wrong. And cannot figure out how to solve the c th question. Questions answers that i got Answers
0
votes
2answers
69 views

“Paradox” involving Hilbert's decision problem

I'm currently reading "Labyrinths of Reason" by William Poundstone. My experience and ability when it comes to mathematics and formal logic is pretty limited, but the book seems to imply the following:...
2
votes
2answers
335 views

Building an Automated Theorem Prover with Machine Learning

I am very interested in developing a machine-learning algorithm that could learn from the axioms, properties of the mathematical system of interest, and positive examples from the conjecture of ...
2
votes
1answer
110 views

Nonstandard Natural Numbers via Internal Set Theory in Coq

I'm trying to translate http://www.stat.umn.edu/geyer/nsa/o.pdf to Coq, but I'm stuck right at the start on the simple axioms for the predicate "standard" over natural numbers. The pdf linked here ...
2
votes
1answer
335 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, ...
6
votes
1answer
78 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 ...
0
votes
0answers
37 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 ...
0
votes
1answer
124 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: ...
1
vote
1answer
72 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 ...
3
votes
1answer
91 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 ...
1
vote
1answer
104 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
37 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
113 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 ...
0
votes
1answer
137 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
238 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
145 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 : (...
7
votes
1answer
104 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
182 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
622 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 ...
8
votes
1answer
335 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 ...
5
votes
2answers
441 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
430 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
377 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
189 views

An impressive fact expressible in Presburger arithmetic?

Is there anything expressible in Presburger arithmetic that would seem impressive to students at an undergraduate level?
17
votes
1answer
711 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
116 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 ...
3
votes
1answer
1k 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?] ...