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
1answer
27 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 ...
0
votes
0answers
30 views

Clause normal form, renaming, and obvious positions

I'm trying to implement a CNF conversion algorithm that handles all cases in linear time, and looking at the question of exactly which subformulas need to be renamed. To this end, I was reading https:/...
0
votes
1answer
37 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 ...
3
votes
2answers
148 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 ...
1
vote
1answer
38 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 (...
2
votes
1answer
188 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) $=...
0
votes
0answers
31 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?
0
votes
0answers
46 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 ...
0
votes
0answers
11 views

Kindly check the PDA transition function, is there any mistake?

I have a CFL language L={$a^nb^m| (n>m), (n,m)>1} and I am trying to get its transition function. Transition diagram for the language L, accepted by final state PDA Please see my transition ...
5
votes
0answers
62 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
1answer
70 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 ...
0
votes
0answers
27 views

TPTP fairness strategy

I need to solve an exercise and I am not sure, what fairness means and how to answer such a question: Consider the following clause selection strategy: Symbols present in the original TPTP conjecture ...
2
votes
1answer
70 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
1answer
46 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
0answers
42 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 ...
6
votes
1answer
77 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
1answer
61 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
1answer
48 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!
5
votes
1answer
235 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
1answer
52 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 ...
1
vote
1answer
38 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
2answers
195 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....
4
votes
1answer
283 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
1answer
44 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
0answers
107 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
434 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
1answer
153 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
1answer
232 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
108 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
307 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
36 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
1answer
39 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 ...
30
votes
8answers
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 ...
4
votes
0answers
70 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
89 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 ...
3
votes
1answer
296 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 ...
2
votes
3answers
151 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
79 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 ...
2
votes
1answer
184 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
133 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
147 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 ...
2
votes
1answer
217 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/~...
5
votes
0answers
188 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
93 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
79 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
433 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 ...
4
votes
1answer
151 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 ...
2
votes
1answer
567 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
88 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
44 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 ...