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
1 vote
0 answers
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 ...
user avatar
  • 11
1 vote
0 answers
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 ...
user avatar
0 votes
2 answers
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 ...
user avatar
0 votes
1 answer
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 ...
user avatar
4 votes
1 answer
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 ...
user avatar
  • 1,498
0 votes
0 answers
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 ...
user avatar
4 votes
1 answer
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 ...
user avatar
0 votes
0 answers
61 views

McDermott about Skolemization

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 ...
user avatar
  • 73
0 votes
1 answer
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 ...
user avatar
  • 109
0 votes
1 answer
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): ...
user avatar
  • 3,216
0 votes
1 answer
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 ...
user avatar
1 vote
2 answers
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 ...
user avatar
  • 49
0 votes
0 answers
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....
user avatar
  • 387
0 votes
1 answer
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 ...
user avatar
  • 2,778
1 vote
1 answer
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 ...
user avatar
  • 1,406
1 vote
1 answer
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 ...
user avatar
  • 463
3 votes
2 answers
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 ...
user avatar
2 votes
1 answer
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 (...
user avatar
  • 463
2 votes
1 answer
609 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) $=...
user avatar
  • 59
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?
user avatar
  • 149
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 ...
user avatar
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,*)$ ...
user avatar
  • 717
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 ...
user avatar
  • 223
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 ...
user avatar
-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 ...
user avatar
  • 9
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 ...
user avatar
  • 1,673
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 ...
user avatar
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 ...
user avatar
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!
user avatar
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 ...
user avatar
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 $\in$ L, x1y Demostrate by induction that a ...
user avatar
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+...
user avatar
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....
user avatar
  • 12k
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 ...
user avatar
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 ...
user avatar
  • 135
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 ...
user avatar
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 ...
user avatar
  • 12k
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 ...
user avatar
  • 12k
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, ...
user avatar
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 ...
user avatar
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:...
user avatar
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 ...
user avatar
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 ...
user avatar
33 votes
8 answers
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 ...
user avatar
  • 3,999
4 votes
0 answers
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?
user avatar
2 votes
0 answers
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 ...
user avatar
3 votes
1 answer
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 ...
user avatar
2 votes
3 answers
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 "...
user avatar
1 vote
0 answers
82 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 ...
user avatar
  • 3,766
2 votes
1 answer
224 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.
user avatar