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

109 questions
Filter by
Sorted by
Tagged with
1 vote
42 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 ...
1 vote
56 views

### Prove that every cycle graph $C_n$ has $n$ edges

I need to prove this directly and by induction. I do not even know where to start. Question: A cycle graph $C_n$ is a connected graph with $n$ vertices, such that each vertex is adjacent to exactly ... 82 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 ...
48 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 ...
104 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 ...
15 views

### is N-Σ-automaton a Non-Deterministic Finite Automata

I am trying to understand a part of this book Automata,Languages and Machines. K=N case I cant undesrtand the Topic because i dont get what a N-Σ-automaton, i tried to find something, but i only get ...
175 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 ...
61 views

I am a beginner in AI. In a paper by McDermott (titled "A critique of pure reason") I found the following passage: "A goal containing a variable is interpreted as a request to find ...
89 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 ...
134 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): ...
93 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 ...
1 vote
68 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 ...
86 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....
77 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 ...
1 vote
34 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 ...
1 vote
73 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 ...
1k 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 ... 62 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 (...
609 views

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) $=... 0 votes 0 answers 40 views ### Theorem proover for set theory I have seen coq as a Theorem Prover, but this is based on type theory asaik. Is there a theorem prover for set theory like coq is for type theory? 1 vote 0 answers 86 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 ... 5 votes 0 answers 74 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,*)$... 2 votes 1 answer 85 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 ... 2 votes 1 answer 98 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 ... -1 votes 1 answer 51 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 ... 1 vote 0 answers 53 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 ... 5 votes 1 answer 87 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 ... 1 vote 1 answer 75 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 ... 0 votes 1 answer 61 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! 6 votes 1 answer 402 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 ... 0 votes 1 answer 53 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$\inL, x1y Demostrate by induction that a ... 2 votes 1 answer 56 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+... 5 votes 2 answers 385 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.... 5 votes 1 answer 404 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 ... 1 vote 1 answer 48 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 ... 8 votes 0 answers 116 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 2 answers 562 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 ... 2 votes 1 answer 201 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 ... 2 votes 1 answer 279 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 1 answer 123 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 1 answer 385 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 1 answer 44 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 ... 1 vote 1 answer 47 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 ...
4k 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 ...
78 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?
106 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 ...
332 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 ...
166 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