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.

Filter by
Sorted by
Tagged with
0 votes
1 answer
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 ...
Amr's user avatar
  • 20.1k
0 votes
0 answers
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 ...
selenio34's user avatar
  • 158
1 vote
2 answers
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 ...
ThePhilosopher's user avatar
2 votes
0 answers
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 ...
Hatchi Roku's user avatar
1 vote
0 answers
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 ...
Salman's user avatar
  • 11
0 votes
1 answer
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 ...
Daniel Donnelly's user avatar
1 vote
0 answers
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/...
user10478's user avatar
  • 1,904
0 votes
0 answers
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 ...
Zahir Bingen's user avatar
0 votes
0 answers
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 ...
Aeryan's user avatar
  • 61
0 votes
0 answers
54 views

Why is this proof of False in the Calculus of Constructions not valid?

So, this would be a definition of False in the Calculus of Constructions: $$\bot = \forall x : \mathbf P . x$$ And, according to Wikipedia, this is an inference rule: $${\Gamma \vdash A : K \qquad \...
Aritz Erkiaga's user avatar
2 votes
1 answer
74 views

Proof of distributivity of $\land$ over $\lor$ using disjE in natural deduction

I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf I'm trying to understand its proof of $$ P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R) $$ ...
Michal Charemza's user avatar
0 votes
3 answers
52 views

Given (non-negative) lists 'x' and 'y', if their means and their standard deviations are the same, does this imply 'x=y'? How can I (simply) prove it?

Let us take a list/vector x and another one y, both of them composed of non-negative integers; e.g., ...
Theo Deep's user avatar
  • 247
2 votes
1 answer
107 views

Mechanizing Herbrand’s theorem

I study automated theorem proving using this book. The author describes mechanizing Herbrand’s theorem by Gilmore procedure: Skolemize negated FOL formula and then tests Herbrand models for ...
Oleg Dats's user avatar
  • 425
1 vote
0 answers
203 views

Unification in first order logic

I know unification problem in first order logic is defined as a equation $t_1=s_1, ..., t_n=s_n$. My question is that why unification in first order logic can not be defined as a unification of a ...
nikkkk's user avatar
  • 31
0 votes
2 answers
85 views

Prove that the set is close

Given metric spaces $(X,d)$ and $(Y,d')$ and continuous mapping $S$ and $T$ from $X$ into $Y$, prove that the set $\{x \in X: Sx = Tx\}$ is closed in $(X,d)$. I've run out of any ideas where I should ...
ae-mathsidk's user avatar
0 votes
1 answer
95 views

Demonstration of proving a statement is unprovable

Similar questions have been asked, but this is not a duplicate. I'm looking for a proof itself, not a description of methods. Related: How do we prove that something is unprovable? is possible to ...
Jeff Hykin's user avatar
5 votes
1 answer
378 views

Existence elimination in Lean 3

Lean 3 is a theorem prover that implements the calculus of inductive constructions. Differently than Coq, Lean 3s kernel works proof irrelevant. This means that in the kernel of Lean all proofs of the ...
Nico's user avatar
  • 4,220
4 votes
1 answer
306 views

Haskell proof checker for FOL with equality

Ignoring issues of efficiency, is this a correct implementation in Haskell of a proof checker for first order logic with equality? I am especially concerned about the ...
user695931's user avatar
0 votes
1 answer
141 views

In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
tribbloid's user avatar
  • 109
0 votes
1 answer
353 views

How does writing proofs in Agda differ from writing them in Isar/Isabelle?

An Isar proof that the square root of 2 is not rational might look like this (according to Wikipedia): ...
Lance's user avatar
  • 3,698
0 votes
1 answer
167 views

Prove that no DFA with two states recognises L.

Consider the language L = {w | the string w starts with an a}, where the string made up of two alphabets {a, b}. Prove that no DFA with two states recognises L. Above is the question. I know it has ...
Business Man's user avatar
1 vote
2 answers
112 views

Counterexample for minimal DFA proof

I'm struggling with a following task: Let $A = (Q, Σ, δ, q_{0}, F)$ be a DFA, in which every state is attainable (attainable ...
jasiu's user avatar
  • 49
0 votes
0 answers
225 views

What is the algorithm for automated theorem proving in intuitionistic propositional logic?

In classical logic exists law of excluded middle: (a or not a). We can append not a to the knowledge base and show contradiction....
Oleg Dats's user avatar
  • 425
0 votes
1 answer
81 views

Deduction in PA that irreducible implies prime

I'm currently showing a few things about $\mathbb{N}$ in the proof assistant Coq, with the goal to take these proofs and turn them into deductions in the first-order theory of PA. One of the open ...
Léreau's user avatar
  • 3,025
1 vote
1 answer
47 views

Why is this language regular?

I'm at the beginning of Theoretical Informatics and I was given some tasks one of which is following... Be $k\in \mathbb{N}$, show that following language $L$ with the alphabet $\Sigma = \{0,1\}$ is ...
Quotenbanane's user avatar
  • 1,594
1 vote
1 answer
105 views

Can we prove any statement in the first order logic operating only in the space of prenex normal forms?

Let's assume that we have a set of statements written in first order logic (axioms and maybe some proven theorems). Now we want to prove that a given "new" statement is true. My naive ...
Roman's user avatar
  • 523
3 votes
2 answers
3k views

Proof Solver Geometry [closed]

Are there any programs that can solve Geometry Problems? An example of such a problem would be: The centroid of a triangle always divides its medians into two sections with a 1:2 ratio. While that ...
user avatar
2 votes
1 answer
97 views

Is there a proof system for first order logic that does not use premisses and auxiliary variables?

Before I have started to learn proof theory for first order logic I had the following simple (and maybe naive) expectations: We can use formal language (first order logic) to formulate expressions (...
Roman's user avatar
  • 523
3 votes
1 answer
2k views

Direct proof - DROP-OUT (A) is a regular language

Proposition: Let A be a regular language over $\Sigma$. Define DROP-OUT(A) to be the language containing all strings that can be obtained by removing one symbol from a string in A. Thus, DROP-OUT(A) $=...
Felipe's user avatar
  • 69
1 vote
0 answers
108 views

Is it not impossible to define self-interpreter in Homotopy Type Theory?

I've been exploring approaches to defining semisimplicial types in a variation of HoTT (as far as I know, it's equivalent to Book HoTT). If this construction succeeded, it would be a major step ...
DrunkCoder's user avatar
5 votes
0 answers
81 views

Is it possible to check the validity of the following theorem in Group Theory automatically by a computer? If so, how?

I'm learning right now how to prove the following very basic theorem in Group Theory, which we learn in a Linear Algebra course in my university (I study Computer Science): Let's have a group $(M,*)$ ...
TKN's user avatar
  • 757
2 votes
1 answer
105 views

Are there any sets of axioms that have an efficient algorithm for all provable statements?

I'm looking for a set of axioms that are reasonably expressive (non-trivial) such that any statement that can be proved as true from the set of axioms can be done so efficiently. By this I mean that ...
Phylliida's user avatar
  • 233
2 votes
1 answer
185 views

Equivalence or Isomorphism of Types

The context I'm working in here is dependent type theory used in proof formalization (in particular in Lean, though is likely not relevant). The question I have is best explained through examples. A ...
Physical Mathematics's user avatar
-1 votes
1 answer
92 views

Proving a shift transformation theorem with taylor series [closed]

I need to prove a transformation theorem $T(ψ(x)) = (e^{hD})*ψ(x)$ and use Taylor series to do this task. It is known that $T(ψ(x)) = ψ(x + h)$ and $D$ is a derivatation. I have no idea, how to start ...
fml's user avatar
  • 9
1 vote
0 answers
76 views

Mathematical logic: What does '?' mean in these Coq (proof-assistant) tactics?

I am new to Mathematical Logic. I am trying to teach myself the Coq proof-assistant from these course notes and some of the inference rules ('tactics') are as follows: What does '?' mean in this ...
user3203476's user avatar
  • 1,763
5 votes
1 answer
120 views

Is an associative binary operation with trivial squares necessarily commutative?

Take a set $S$ and an associative binary operation $*:S \times S \rightarrow S$ such that there exists an element $e$ such that $x * x = e$ for any $x \in S$. Can we conclude that the operation is ...
M. Rinetti's user avatar
1 vote
1 answer
100 views

Can computer use the Henkin method?

To prove completeness of First order logic,we have Henkin's method to build a Maximal consistent modal to satisfy a consistent set of formulae. How can we formalize Henkin method(in the sense that we ...
XXX's user avatar
  • 225
0 votes
2 answers
102 views

What paper proved the completeness of Ordered Resolution?

I am having trouble finding online the original proof of the completeness of Ordered Resolution. Does anyone happen to know where it exists? Thanks!
user1050268's user avatar
7 votes
1 answer
601 views

Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF?

Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF? If you took your average mathematician on the street and tried to pin down the axiomatics they are implicitly using they'd ...
Physical Mathematics's user avatar
0 votes
1 answer
54 views

Estructural inductionin

L is the lowest set of string under the following rules: 1) 1 $\in$ L 2) If x $\in$ L, 0x $\in$ L 3) If x $\in$ L, x0 $\in$ L 4) If x $\in$ L and y $\in$ L, x1y Demostrate by induction that a ...
Rodo Mendoza Lúcar's user avatar
2 votes
1 answer
67 views

Automating the solution of pairs of polynomial inequalities as a bound

Let's consider the following pair of quadratic inequalities: $$\begin{aligned} x^2+x &\geq a\\ x^2-x &< a\end{aligned}$$ The solution of the first inequality is $$\left( x \geq \frac{-1+...
Kristada673's user avatar
6 votes
3 answers
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....
user56834's user avatar
  • 13k
7 votes
1 answer
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 ...
Ram Rachum's user avatar
1 vote
1 answer
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 ...
Reubend's user avatar
  • 135
8 votes
0 answers
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 ...
Elliott Macneil's user avatar
6 votes
2 answers
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 ...
user56834's user avatar
  • 13k
2 votes
1 answer
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 ...
user56834's user avatar
  • 13k
2 votes
1 answer
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, ...
michalk93's user avatar
0 votes
1 answer
132 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 ...
Laurentiu's user avatar
2 votes
1 answer
467 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:...
Kliker's user avatar
  • 79