# 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.

118 questions
Filter by
Sorted by
Tagged with
161 views

### Are there attempts to use machine learning to settle disputes over long mathematical proofs?

As far as I remember, The proof of Perelman of the Geometerization Conjecture took a year to check by the experts. The claimed proof of the ABC conjecture Mochizuki took few years to check, and Peter ...
• 20.1k
34 views

### First order logic formalization problem

I have to formalize the following problem for the SPASS theorem prover (first order logic): "On an island there are exactly two type of people: knights, who always say the truth, and knaves, who ...
• 158
1 vote
106 views

### Is someone trying to solve problems by building all possible proofs using all possible rules of inference? [closed]

We obviously can construct a program that, starting with ZFC (or any other theory) axioms, would use all possible rules of inference to get all possible proofs constructible in ZFC. (There would be ...
130 views

### Can we prove every provable statement with lean?

I just discovered Lean and using computers for stating and proving theorems. The first question that came to my mind, can we write any proof with Lean? Or are there limitations (something that you can ...
• 187
1 vote
79 views

### Unification when multiple copies of a formula are needed

I'm coming from a logic and philosophy of logic background and am becoming more and more interested in comparing human theorem proving and automated theorem proving (ATP). At this stage, I'm trying to ...
• 11
59 views

### Can you exhibit a 3rd-or-higher order logical formula that has no "Prenex normal form"?

The Prenex normal form is a canonical form for logical formulas in 1st & 2nd order logic. I've read that higher order logic has no such thing that can be computed. However, I'm wondering what ...
• 21.4k
1 vote
53 views

### What is the best way to manipulate probability expressions in code?

Suppose I want to write code to derive formulas using basic algebra and rules of probability theory (general multiplication rule, inclusion-exclusion, law of total probability, conversion to odds/...
• 1,904
50 views

### Proving (a ↔ a) → a in LEAN3

I'm trying to proof (a ↔ a) → a in lean, but I can't figure out which lemmas/tactics to use. Proving a → (a ↔ a) is something I can do. Can someone guide me with the steps necessary to take to solve ...
31 views

### Can the resolution algorithm be applied to any FOL formula?

I have been searching for an automatic method (a computer program) to evaluate any first-order logic (FOL) formula given some knowledge base. The most common approach to do this is to use PROLOG. The ...
• 61
54 views

• 555
567 views

### Difference between $\lambda$-$\mu$-calculus and intuitionistic type theory + LEM for classical proofs?

I have some experience with using type theory to do proofs in intuitionistic logic. If I want to prove theorems that require classical logic, I simply pose the law of excluded middle (LEM) as an axiom....
• 13k
579 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 ...
• 187
1 vote
56 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 ...
• 135
126 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 ...
811 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 ...
• 13k
295 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 ...
• 13k
340 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, ...
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 ...
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:...