Questions tagged [automated-theorem-proving]
Automated theorem proving is the proving of mathematical theorems by a computer program.
47
questions
37
votes
2
answers
2k
views
If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?
This is a naive question, out of my expertise; apologies in advance.
Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For ...
- 3,753
29
votes
1
answer
936
views
Is there a reasonable automated proof system for TCS theorems?
Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
user1338
18
votes
4
answers
858
views
Automated theorem proving in linear logic
Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction?
Where can I read more about automatic theorem proving in these ...
- 4,041
18
votes
2
answers
2k
views
Why is it so difficult for a computer to prove something?
This may be considered a stupid question. I am not a computer science major (and I'm not a mathematics major yet, either), so please excuse me if you think that the following questions display some ...
- 647
15
votes
1
answer
588
views
Logical Reations for an Impredicative System in a Predicative MetaTheory
Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
- 1,685
15
votes
1
answer
278
views
How to determine whether a proof requires "higher-order reasoning techniques"?
The question:
Suppose I have a specification of a problem consisting of axioms and a goal (i.e. the associated proof problem is whether the goal is satisfiable given all the axioms). Let us also ...
- 159
14
votes
6
answers
686
views
What are practically computable properties of Labelled Transition Systems?
I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
- 241
12
votes
2
answers
459
views
State of the Art for the Monadic Class?
Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.
...
- 2,832
12
votes
0
answers
237
views
Have any well-known results been refuted by a theorem prover?
Have any well-known results in mathematics or computer science been shown to be false through the use of a theorem prover or proof assistant? I am not interested in cases where the proof of a true ...
- 221
11
votes
3
answers
633
views
Proofs found by computer
In 1996, a long-standing open problem was solved by a computer; namely, that Robbins algebra and Boolean algebra are the same. The proof was found by an automated theorem prover.
Moreover, the known ...
- 4,031
11
votes
2
answers
1k
views
What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?
I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
- 279
10
votes
2
answers
481
views
Are there semi-decision procedures for this theory?
I have the following typed theory
|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)
...
- 221
10
votes
1
answer
900
views
Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory.
The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
- 2,581
9
votes
1
answer
677
views
Why is Proof Checker required in Proof Carrying Code
In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:
VCGen to generate verification conditions (safety predicates)
First-...
- 193
9
votes
2
answers
1k
views
Automated theorem proving via unsupervised approaches
This question Where and how did computers help prove a theorem? considers some automated theorem proving successes.
However they seem to be mostly supervised approaches, such as with the 4 color graph ...
- 11k
9
votes
1
answer
624
views
First order satisfiability that doesn't have finite models
We know from Church's theorem that determining first order satisfiability is undecidable in general, but there are several techniques we can use to determine first order satisfiability. The most ...
- 318
9
votes
1
answer
435
views
Turing Machines as Coalgebras
I'm looking to write a survey on the method of representing the dynamics of state-based computation within the framework of coalgebras. So far I've managed to find papers on coalgebra representations ...
- 163
8
votes
1
answer
235
views
What is the significance of nominal techniques?
What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned?
I have been reading M. J. Gabbay's expository work on the topic that ...
8
votes
0
answers
224
views
Is there a known automatic proof of the independence of the continuum hypothesis?
In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence ...
- 181
7
votes
1
answer
228
views
Formalized priority argument
A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce ...
- 895
6
votes
1
answer
574
views
reference for lexicographic path ordering
Can you recommend a good reference for reading about lexicographic/recursive path orderings?
I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem ...
- 189
6
votes
1
answer
291
views
General Induction Principle
Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals:
...
- 175
5
votes
1
answer
249
views
Mechanization of Mathematics
Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false.
By the completeness theorem of first-order logic, a statement is universally valid ...
- 87
5
votes
1
answer
304
views
What's the state of research on automated theorem proving?
I'm interested in writing my undergraduate thesis on automated theorem proving, and I've been looking for some material to document myself on the topic.
I was introduced to automated and assisted ...
- 161
5
votes
0
answers
121
views
extracting/ exploiting similarity of SAT instances by solver
suppose that two SAT formulas on different variables $F_1, F_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas ...
- 11k
5
votes
0
answers
305
views
Are there applications of experimental mathematics in TCS?
In recent years there have been major, diverse, sometimes surprising advances in experimental mathematics [1] for a variety of sophisticated uses such as developing/deriving exact formulas, theorem ...
- 11k
4
votes
1
answer
387
views
If a root||nonce Proof-of-Work certificate is prime, can it be used in any other interesting proofs?
Because Bitcoin and many other cryptocurrency mining certificates are "rare" in that their respective hash is less than a very small number, can we leverage their rarity in probabilistic proofs of ...
- 1,083
4
votes
1
answer
239
views
resolution based theorem prover for temporal logic
I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
- 181
4
votes
1
answer
263
views
Looking for reference on NP-Completeness of proofs of length n
Given a deductive system $\Lambda$, and some well-formed-formula S, one can ask the question "Is there a proof S in $\Lambda$ of length n?" If n is presented in base-1 and if all the axioms of $\...
- 425
4
votes
0
answers
199
views
What logic do refinement types correspond to?
I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
- 41
4
votes
0
answers
142
views
A reasonable proof strategy for formally verifying Ukkonen's algorithm?
What's a reasonable proof strategy to formally verify Ukkonen's algorithm in, say, Coq? The ingredients as far as I can tell would be:
some form of separation logic to be able to reason about the ...
- 595
4
votes
0
answers
522
views
Is it possible to derive induction by extending CoC with recursion?
Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms:
...
- 3,137
3
votes
3
answers
333
views
Automatic proofs or model checking in an extremely simplified functional language
Imagine a stripped down functional programming language, that has the following properties
The only value type is an integer
There are no side effects
Functions are defined as a single expression, ...
- 185
3
votes
1
answer
159
views
Can we verify satisfiability of first order statements via saturation in sub-exponential time?
In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the ...
- 318
2
votes
1
answer
408
views
Extensional type theory and function extensionality
Is the principle of function extensionality
$ (\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT?
Most notably is this derivable in Agda with axiom K?
- 920
2
votes
2
answers
877
views
Which formalism is best suited for automated theorem proving in set theory?
Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving.
Context ...
- 279
2
votes
1
answer
129
views
How to auto-derivate sequential iterative programs from a mathematical specification?
I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.
First, write down the formal specification as a Hoare triple and figure ...
- 23
2
votes
2
answers
430
views
Automated proving that a program doesn't halt
If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
- 145
2
votes
0
answers
390
views
Theorem prover fails to find simple set theory proof?
I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic.
Tarski claims in his "a work on mereology" that
the goal is provable from assertions 1-3 but he does ...
- 279
2
votes
0
answers
79
views
Regaining decidability by adding axioms that model real world situation
It is known that first order logic is too general to be decidable. Adding axioms with special meaning (e.g. expressing notions such as necessity/obligation, provability, etc.) leads us to modal logics ...
- 409
1
vote
0
answers
83
views
Journals or conferences to submit formally verified libraries?
This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of:
synthetic differential ...
- 595
1
vote
0
answers
155
views
Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP
In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
- 21
0
votes
1
answer
199
views
Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?
Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem？ In other words, could the Tarski–Seidenberg theorem subsume Buchberger's algorithm and Wu's ...
- 1,070
0
votes
1
answer
311
views
Automatic theorem prover for first-order logic versus model checker
What's the formal difference between a model checker, and an automated theorem prover for first-order logic, i.e. something like Meson/Metis/Sledgehammer/Vampire/E? Link to a clear discussion of the ...
- 920
0
votes
1
answer
192
views
Is there an algorithm to generate proof in Coq? [closed]
I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie, to specify an insertion ...
- 159
0
votes
2
answers
235
views
Logic with Linear Programming
Can first-order logic be modeled/simulated as linear programming or integer programming?
What about other forms of logic (say second order)?
Update: am actually not a theory person, but more on the ...
- 749
-5
votes
1
answer
3k
views
Proof that DFA that accepts string has NFA that accepts reversal of string
I have seen descriptions for an algorithm that can take a regular deterministic finite automata and create a non-deterministic finite automata that is guaranteed to generate the reverse of string ...
- 7